Accéder directement au contenu

Guillaume Melquiond

4
Documents

Publications

catherine-lelay
Image document

Formalization of Real Analysis: A Survey of Proof Assistants and Libraries

 Sylvie Boldo , Catherine Lelay , Guillaume Melquiond
Mathematical Structures in Computer Science, 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩
Article dans une revue hal-00806920v2
Image document

Coquelicot: A User-Friendly Library of Real Analysis for Coq

 Sylvie Boldo , Catherine Lelay , Guillaume Melquiond
Mathematics in Computer Science, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩
Article dans une revue hal-00860648v2
Image document

Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert

 Catherine Lelay , Guillaume Melquiond
JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France
Communication dans un congrès hal-00642206v2
Image document

Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives

 Sylvie Boldo , Catherine Lelay , Guillaume Melquiond
CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. pp.289-304, ⟨10.1007/978-3-642-35308-6_22⟩
Communication dans un congrès hal-00712938v2