Skip to Main content Skip to Navigation

inria-00407778v1  Reports
Georges GonthierRoux Stéphane Le. An Ssreflect Tutorial
[Technical Report] RT-0367, INRIA. 2009, pp.33
hal-01671777v3  Journal articles
Matthieu SozeauCyprien Mangin. Equations reloaded
Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (ICFP), pp.1-29. ⟨10.1145/3341690⟩
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⟩
hal-01091189v2  Journal articles
Pierre Roux. Formal Proofs of Rounding Error Bounds
Journal of Automated Reasoning, Springer Verlag, 2015, pp.23. ⟨10.1007/s10817-015-9339-z⟩
hal-02536463v2  Journal articles
Guillaume AmbalSergueï LengletAlan Schmitt. HOπ in Coq
Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-020-09553-0⟩
inria-00118903v1  Journal articles
Julien Narboux. A Graphical User Interface for Formal Proofs in Geometry.
Journal of Automated Reasoning, Springer Verlag, 2007, Special Issue on User Interfaces in Theorem Proving, 39 (2), pp.161-180. ⟨10.1007/s10817-007-9071-4⟩
pastel-00780446v1  Theses
Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
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-00763495v1  Conference papers
Frédéric BlanquiKim Quyen Ly. Automated verification of termination certificates
15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam
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-01350254v1  Journal articles
Benjamin Werner. Preuves formelles, preuves calculatoires
Interstices, INRIA, 2007
hal-01350404v1  Journal articles
Benjamin Werner. La vérité et la machine
Interstices, INRIA, 2009
hal-01265666v1  Conference papers
Arthur Azevedo de AmorimMaxime DénèsNick GiannarakisCătălin HriţcuBenjamin Pierce et al.  Micro-Policies: Formally Verified, Tag-Based Security Monitors
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, ⟨10.1109/SP.2015.55⟩
hal-02101787v1  Reports
Judicael Courant. Proof reconstruction (preliminary version).
[Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p
hal-01518660v1  Conference papers
Nicolas Magaud. Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Jan 2017, Paris, France. ⟨10.1145/nnnnnnn.nnnnnnn⟩
inria-00464237v3  Conference papers
Cyril CohenAssia Mahboubi. A formal quantifier elimination for algebraically closed fields
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. pp.189-203, ⟨10.1007/978-3-642-14128-7_17⟩
inria-00473270v1  Conference papers
Pieter CollinsMilad NiquiNathalie Revol. A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq
NSV-3: Third International Workshop on Numerical Software Verification., Fainekos, Georgios and Goubault, Eric and Putot, Sylvie, Jul 2010, Edinburgh, United Kingdom
hal-00816918v1  Preprints, Working Papers, ...
Pierre Boutillier. Simple simpl
hal-00730913v1  Conference papers
Chantal KellerMarc Lasson. Parametricity in an Impredicative Sort
CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, Sep 2012, Fontainebleau, France. pp.381-395, ⟨10.4230/LIPIcs.CSL.2012.399⟩
pastel-00605836v1  Theses
Arnaud Spiwack. Verified Computing in Homological Algebra
Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English
ensl-00560449v1  Conference papers
Érik Martin-Dorel. Formalization of Hensel's lemma in Coq
TYPES 2010: The 17th Workshop on Types for Proofs and Programs, Oct 2010, Warsaw, Poland
hal-02102015v1  Reports
Sylvie BoldoMarc Daumas. A simple test qualifying the accuracy of Horner's rule for polynomials
[Research Report] LIP RR-2003-01, Laboratoire de l'informatique du parallélisme. 2003, 2+39p
hal-02101979v1  Reports
Sylvie BoldoGuillaume Melquiond. When double rounding is odd
[Research Report] LIP RR-2004-48, Laboratoire de l'informatique du parallélisme. 2004, 2+7p
inria-00001035v1  Conference papers
Julien Narboux. A Decision Procedure for Geometry in Coq
Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. pp.225-240, ⟨10.1007/b100400⟩
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-01630411v1  Conference papers
Florian Faissole. Formalization and closedness of finite dimensional subspaces
SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
hal-01244578v1  Reports
Andrei ArusoaieDavid NowakVlad RusuDorel Lucanu. Formal Proof of Soundness for an RL Prover
[Technical Report] RR-0471, INRIA Lille - Nord Europe; Alexandru Ioan Cuza, University of Iasi. 2015, pp.27
hal-00671809v2  Conference papers
Cyril Cohen. Construction of real algebraic numbers in Coq
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States