 |
 |
 |
|
|
||
|---|---|---|
| |
||
| hal-01671777v3
Journal articles
Equations reloaded Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (ICFP), pp.1-29. ⟨10.1145/3341690⟩ |
||
| 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⟩  |
||
| hal-01091189v2
Journal articles
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
HOπ in Coq Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-020-09553-0⟩ |
||
| inria-00118903v1
Journal articles
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
Formalized algebraic numbers: construction and first-order theory. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English |
||
| 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-00763495v1
Conference papers
Automated verification of termination certificates 15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam |
||
| 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-01265666v1
Conference papers
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-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-02101787v1
Reports
Proof reconstruction (preliminary version). [Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p |
||
| hal-01518660v1
Conference papers
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
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
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-00730913v1
Conference papers
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
Verified Computing in Homological Algebra Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English |
||
| 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⟩ |
||
| ensl-00560449v1
Conference papers
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
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
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
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
Les assistants de preuve, ou comment avoir confiance en ses démonstrations. Séminaire L, Mar 2013, Strasbourg, France |
||
| hal-01630411v1
Conference papers
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
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
Construction of real algebraic numbers in Coq ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States |
||
|
|
||