Nombre de documents

7

CV de Catherine Lelay


Article dans une revue2 documents

  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Formalization of Real Analysis: A Survey of Proof Assistants and Libraries. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 26 (7), pp.1196-1233. <10.1017/S0960129514000437>. <hal-00806920v2>
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. <10.1007/s11786-014-0181-1>. <hal-00860648v2>

Communication dans un congrès4 documents

  • Catherine Lelay. How to express convergence for analysis in Coq. The 7th Coq Workshop, Jun 2015, Sophia Antipolis, France. <hal-01169321>
  • Catherine Lelay. A New Formalization of Power Series in Coq. The 5th Coq Workshop, Jul 2013, Rennes, France. 2013, <http://coq.inria.fr/coq-workshop/2013>. <hal-00880212>
  • Catherine Lelay, Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. <hal-00642206v2>
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. Chris Hawblitzel and Dale Miller. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. Springer, 7679, pp.289-304, 2012, Lecture Notes in Computer Science; Certified Programs and Proofs. <10.1007/978-3-642-35308-6_22>. <hal-00712938v2>

Thèse1 document

  • Catherine Lelay. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée. Autre [cs.OH]. Université Paris Sud - Paris XI, 2015. Français. <NNT : 2015PA112096>. <tel-01228517>