 |
 |
 |
|
|
||
|---|---|---|
| inria-00390902v1
Reports
Automated Verification of Termination Certificates [Research Report] RR-6949, INRIA. 2009, pp.24 |
||
| hal-02101837v1
Reports
Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq [Research Report] LIP RR-2002-14, Laboratoire de l'informatique du parallélisme. 2002, 2+36p |
||
| hal-02333423v1
Conference papers
Certification of Breadth-First Algorithms by Extraction 13th International Conference on Mathematics of Program Construction, MPC 2019, Oct 2019, Porto, Portugal. pp.45-75, ⟨10.1007/978-3-030-33636-3_3⟩ |
||
| tel-01944510v3
Theses
Verifying constant-time implementations in a verified compilation toolchain Cryptography and Security [cs.CR]. Université Rennes 1, 2018. English. ⟨NNT : 2018REN1S099⟩ |
||
| hal-02972245v2
Journal articles
Formalization of double-word arithmetic, and comments on "Tight and rigorous error bounds for basic building blocks of double-word arithmetic ACM Transactions on Mathematical Software, Association for Computing Machinery, 2022, 48 (1), pp.1-24. ⟨10.1145/3484514⟩ |
||
| inria-00099931v1
Reports
Proposition d'architecture du moteur de test de conversion [Contrat] A04-R-488 || blanqui04d, 2004, 7 p |
||
| hal-03471095v1
Journal articles
A Coq Formalization of Lebesgue Integration of Nonnegative Functions Journal of Automated Reasoning, Springer Verlag, In press, ⟨10.1007/s10817-021-09612-0⟩ |
||
| pastel-00649586v1
Theses
Generic Proof Tools and Finite Group Theory Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2011. English |
||
| hal-00809448v1
Documents associated with scientific events
Les assistants de preuve, ou comment avoir confiance en ses démonstrations. Séminaire L, Mar 2013, Strasbourg, France |
||
| hal-00150915v1
Conference papers
Formalizing Stalmarck's algorithm in Coq Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, 2000, Portland, United States. pp.388 |
||
| hal-01391578v1
Conference papers
A Coq formal proof of the Lax–Milgram theorem 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩ |
||
| hal-03517003v1
Journal articles
A formal proof of the irrationality of ζ(3) Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, 17 (1), pp.1-25. ⟨10.23638/LMCS-17(1:16)2021⟩ |
||
| hal-03543701v2
Reports
Stating and Handling Semantics with Skel and Necro [Research Report] RR-9449, Inria Rennes - Bretagne Atlantique. 2022, pp.1-23 |
||
| hal-01421212v1
Conference papers
The HoTT Library CPP'17, ACM, Jan 2017, Paris, France. pp.9, ⟨10.1145/3018610.3018615⟩  |
||
| hal-00779752v1
Conference papers
Un régime au concentré d'automate JFLA - Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France |
||
| hal-00776876v1
Conference papers
Formal Verification of Hardware Synthesis Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. pp.213-228, ⟨10.1007/978-3-642-39799-8_14⟩ |
||
| hal-00937168v1
Conference papers
Handcrafted Inversions Made Operational on Operational Semantics ITP 2013 - 4th International Conference Interactive Theorem Proving, Jul 2013, Rennes, France. pp.338-353, ⟨10.1007/978-3-642-39634-2_25⟩ |
||
| tel-00523810v1
Theses
Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. Autre [cs.OH]. Université Pierre et Marie Curie - Paris VI, 1999. Français |
||
| inria-00160309v2
Reports
Theorem proving support in programming language semantics [Research Report] RR-6242, INRIA. 2007, pp.23 |
||
| hal-03525711v1
Journal articles
Modular, compositional, and executable formal semantics for LLVM IR Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1-30. ⟨10.1145/3473572⟩ |
||
| hal-03107526v1
Journal articles
Modular verification of programs with effects and effects handlers Formal Aspects of Computing, Springer Verlag, 2020, ⟨10.1007/s00165-020-00523-2⟩ |
||
| hal-02333404v1
Conference papers
Hilbert's Tenth Problem in Coq 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Jun 2019, Dortmund, Germany. pp.27:1--27:20, ⟨10.4230/LIPIcs.FSCD.2019.27⟩ |
||
| hal-02536463v2
Journal articles
HOπ in Coq Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-020-09553-0⟩ |
||
| hal-02478907v5
Conference papers
Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.34:1--34:21, ⟨10.4230/LIPIcs.FSCD.2020.34⟩ |
||
| hal-01559073v6
Journal articles
Equivalences for Free Proceedings of the ACM on Programming Languages, ACM, 2018, ICFP'18, 2 (ICFP), pp.1-29. ⟨10.1145/3234615⟩ |
||
| hal-01671994v1
Conference papers
Coq's Prolog and application to defining semi-automatic tactics Type Theory Based Tools, Jan 2017, Paris, France |
||
| hal-01319066v1
Conference papers
The Definitional Side of the Forcing Logics in Computer Science, May 2016, New York, United States. ⟨10.1145/http://dx.doi.org/10.1145/2933575.2935320⟩ |
||
| tel-01890983v1
Theses
Program in Coq Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2018. English |
||
| hal-01890511v1
Journal articles
Mtac2: typed tactics for backward reasoning in Coq Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.1 - 31. ⟨10.1145/3236773⟩  |
||
| tel-01445821v1
Habilitation à diriger des recherches
Automata for relation algebra and formal proofs Computer Science [cs]. ENS Lyon, 2016 |
||
|
|
||
