Skip to Main content Skip to Navigation

hal-02975012v1  Journal articles
Gilles BartheSandrine BlazyBenjamin GrégoireRémi HutinVincent Laporte et al.  Formal verification of a constant-time preserving C compiler
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
hal-01112084v1  Conference papers
Gilles BartheBenjamin GrégoireYassine LakhnechSantiago Zanella-Béguelin. Beyond Provable Security Verifiable IND-CCA Security of OAEP
Topics in Cryptology - 2011 - The Cryptographers' Track at the Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings, 2011, San Francisco, United States. ⟨10.1007/978-3-642-19074-2_13⟩
tel-02333396v2  Theses
Damien Rouhling. Formalisation tools for classical analysis : a case study in control theory
Logic in Computer Science [cs.LO]. Université Côte d'Azur, 2019. English. ⟨NNT : 2019AZUR4058⟩
inria-00258384v17  Reports
Georges GonthierAssia MahboubiEnrico Tassi. A Small Scale Reflection Extension for the Coq system
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
hal-00816699v1  Conference papers
Georges GonthierAndrea AspertiJeremy AvigadYves BertotCyril Cohen et al.  A Machine-Checked Proof of the Odd Order Theorem
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
inria-00585203v1  Conference papers
Tuan Minh Pham. Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs
SAC 2010 - 25th ACM International Symposium on Applied Computing, Mar 2010, Sierre, Switzerland. ⟨10.1145/1774088.1774358⟩
inria-00277075v2  Conference papers
Yves BertotEkaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq
Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary
hal-00765883v1  Conference papers
Michael BackesGilles BartheMatthias BergBenjamin GrégoireCesar Kunz et al.  Verified Security of Merkle-Damgaard
25th IEEE Computer Security Foundations Symposium, CSF 2012, Jun 2012, Cambridge, MA, United States. pp.354-368, ⟨10.1109/CSF.2012.14⟩
hal-00864827v1  Journal articles
Julianna Zsidó. Theorem of three circles in Coq
Journal of Automated Reasoning, Springer Verlag, 2013, ⟨10.1007/s10817-013-9299-0⟩
hal-01647563v1  Conference papers
Sophie Bernard. Formalization of the Lindemann-Weierstrass Theorem
Interactive Theorem Proving, Sep 2017, Brasilia, Brazil
hal-00639130v1  Conference papers
Michaël ArmandGermain FaureBenjamin GrégoireChantal KellerLaurent Théry et al.  A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩
inria-00138382v2  Conference papers
Laurent ThéryGuillaume Hanrot. Primality Proving with Elliptic Curves
TPHOL 2007, Sep 2007, Kaiserslautern, Germany. pp.319-333
hal-01410567v3  Journal articles
Ferruccio GuidiClaudio Sacerdoti CoenEnrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2019, 29 (8), pp.1125-1150
hal-00937197v1  Conference papers
Qian WangBruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories
Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. pp.653--667, ⟨10.4230/LIPIcs.CSL.2013.653⟩
inria-00116820v2  Conference papers
Nicolas Julien. Arithmétique réelle exacte certifiée, co-induction et base arbitraire
Journées Francophones des Langages Applicatifs, Jan 2007, Aix-les-Bains
hal-00537104v1  Conference papers
Benjamin GrégoireJorge Sacchini. On Strong Normalization of the Calculus of Constructions with Type-Based Termination
17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Oct 2010, Yogyakarta, Indonesia. pp.333-347, ⟨10.1007/978-3-642-16242-8_24⟩
hal-00734505v1  Conference papers
Maxime DénèsAnders MörtbergVincent Siles. A refinement-based approach to computational algebra in COQ
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. pp.83-98, ⟨10.1007/978-3-642-32347-8_7⟩
inria-00322331v4  Conference papers
Yves BertotEkaterina Komendantskaya. Using Structural Recursion for Corecursion
Types 2008, 2008, Torino, Italy. pp.220-236