Skip to Main content Skip to Navigation


...
hal-01356690v1  Reports
Thomas LetanPierre ChifflierGuillaume HietPierre NéronBenjamin Morin. SpecCert: Specifying and Verifying Hardware-based Security Enforcement
[Technical Report] CentraleSupélec; Agence Nationale de Sécurité des Systèmes d’Information. 2016, pp.20
...
hal-02422273v1  Conference papers
Thomas LetanYann Régis-Gianas. FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, Nouvelle-Orléans, United States. pp.1-15, ⟨10.1145/3372885.3373812⟩
...
hal-01799712v1  Conference papers
Thomas LetanYann Régis-GianasPierre ChifflierGuillaume Hiet. Modular Verification of Programs with Effects and Effect Handlers in Coq
FM 2018 - 22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.338-354, ⟨10.1007/978-3-319-95582-7_20⟩