Skip to Main content Skip to Navigation
  1. Search


hal-02975012v1  Journal articles
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent 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-01719918v3  Journal articles
Reynald Affeldt, Cyril Cohen, Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis
Journal of Formalized Reasoning, ASDD-AlmaDL, 2018
...
hal-02404581v1  Conference papers
José Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir et al.  Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
CCS 2019 - 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩
hal-01112084v1  Conference papers
Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago 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 Gonthier, Assia Mahboubi, Enrico 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 Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril 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 Bertot, Ekaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq
Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary
...
hal-00765883v1  Conference papers
Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, Cesar 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-01074927v1  Conference papers
Yves Bertot. Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations
Certified Programs and Proofs (CPP'15), Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693172⟩
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 Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent 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éry, Guillaume Hanrot. Primality Proving with Elliptic Curves
TPHOL 2007, Sep 2007, Kaiserslautern, Germany. pp.319-333
...
hal-01410567v3  Journal articles
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico 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-02088293v1  Preprints, Working Papers, ...
Florian Steinberg, Laurent Théry, Holger Thies. Quantitative continuity and computable analysis in Coq
2019
hal-00937197v1  Conference papers
Qian Wang, Bruno 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égoire, Jorge 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⟩
...
inria-00139131v2  Reports
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory
[Research Report] RR-6156, INRIA. 2007, pp.17
...
hal-00734505v1  Conference papers
Maxime Dénès, Anders Mörtberg, Vincent 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 Bertot, Ekaterina Komendantskaya. Using Structural Recursion for Corecursion
Types 2008, 2008, Torino, Italy. pp.220-236
...
inria-00295027v2  Conference papers
Ekaterina Komendantskaya, John Power. Fibrational semantics for many-valued logic programs: grounds for non-groundness.
JELIA, Aug 2008, Dresden, Germany
...
inria-00408143v7  Reports
José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets
[Research Report] RR-6999, INRIA. 2013, pp.213