Skip to Main content Skip to Navigation


...
hal-02101837v1  Reports
Jean Duprat. 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
Dominique Larchey-WendlingRalph Matthes. 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
Alix Trieu. Verifying constant-time implementations in a verified compilation toolchain
Cryptography and Security [cs.CR]. Université Rennes 1, 2018. English. ⟨NNT : 2018REN1S099⟩
...
pastel-00649586v1  Theses
François Garillot. 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
Julien Narboux. Les assistants de preuve, ou comment avoir confiance en ses démonstrations.
Séminaire L, Mar 2013, Strasbourg, France
...
hal-00150915v1  Conference papers
Pierre LetouzeyLaurent Théry. 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
Sylvie BoldoFrançois ClémentFlorian FaissoleVincent MartinMicaela Mayero. 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
Assia MahboubiThomas Sibut-Pinote. 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
Louis NoizetAlan Schmitt. Stating and Handling Semantics with Skel and Necro
[Research Report] RR-9449, Inria Rennes - Bretagne Atlantique. 2022, pp.1-23
hal-01421212v1  Conference papers
Andrej BauerGross JasonPeter LumsdaineMichael ShulmanMatthieu Sozeau et al.  The HoTT Library
CPP'17, ACM, Jan 2017, Paris, France. pp.9, ⟨10.1145/3018610.3018615⟩
...
hal-00779752v1  Conference papers
Pierre-Marie Pédrot. 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
Thomas BraibantAdam Chlipala. 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
Jean-François MoninXiaomu Shi. 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⟩
...
inria-00160309v2  Reports
yves Bertot. Theorem proving support in programming language semantics
[Research Report] RR-6242, INRIA. 2007, pp.23
...
hal-03525711v1  Journal articles
yannick ZakowskiCalvin BeckIrene yoonIlia ZaichukVadim Zaliva et al.  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-02333404v1  Conference papers
Dominique Larchey-Wendlingyannick Forster. 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
Guillaume AmbalSergueï LengletAlan Schmitt. HOπ in Coq
Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-020-09553-0⟩
...
hal-02478907v5  Conference papers
Cyril CohenKazuhiko SakaguchiEnrico Tassi. 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
Nicolas TabareauÉric TanterMatthieu Sozeau. 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
Théo ZimmermannHugo Herbelin. Coq's Prolog and application to defining semi-automatic tactics
Type Theory Based Tools, Jan 2017, Paris, France
...
tel-01890983v1  Theses
Guillaume Claret. Program in Coq
Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2018. English
hal-01890511v1  Journal articles
Jan-Oliver KaiserBeta ZilianiRobbert Krebbersyann Régis-GianasDerek Dreyer. 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
Damien Pous. Automata for relation algebra and formal proofs
Computer Science [cs]. ENS Lyon, 2016