[1] Yves Bertot and Pierre Castéran. Coq'Art: examples and exercises. http://www.labri.fr/Perso/~casteran/CoqArt. [ bib ]
[2] Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin, editors. Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings. Springer. [ bib ]
[3] Masami Hagiya and Philip Wadler, editors. Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings. [ bib ]
[4] Laurent Théry, Yves Bertot, and Gilles Kahn. Real Theorem Provers Deserve Real User-Interfaces. Software Engineering Notes, 17(5), 1992. Proceedings of the 5th Symposium on Software Development Environments. [ bib ]
[5] Yves Bertot, Gilles Kahn, and Laurent Théry. Proof by pointing. In Theoretical Aspects of Computer Software, volume 789 of LNCS, pages 141-160, 1994. [ bib ]
[6] Yann Coscoy, Gilles Kahn, and Laurent Théry. Extracting text from proofs. In TLCA, volume 902 of LNCS, pages 109-123, 1995. [ bib ]
[7] Yves Bertot and Ranan Fraer. Reasoning with Executable Specifications. In Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT'95), volume 915 of LNCS, pages 531-545, 1995. [ bib ]
[8] Laurence Rideau and Laurent Théry. Interactive programming environment for ml. Rapport de recherche RR-3139, INRIA, 1997. [ bib | .html ]
[9] John Harrison and Laurent Théry. A skeptic's approach to combining hol and maple. J. Autom. Reasoning, 21(3):279-294, 1998. [ bib ]
[10] Yves Bertot. A certified compiler for an imperative language. Research report RR-3488, INRIA, 1998. [ bib ]
[11] Laurent Théry. A certified version of Buchberger's algorithm. In Automated Deduction-CADE-15, volume 1421 of Lecture Notes in Artificial Intelligence, pages 349-364. Springer-Verlag, 1998. [ bib ]
[12] Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25:161-194, 1998. [ bib ]
[13] Olivier Pons, Yves Bertot, and Laurence Rideau. Notions of dependency in proof assistants. In User Interfaces for Theorem Provers 1998, Eindhoven University of Technology, 1998. [ bib ]
[14] Olivier Pons. Conception et réalisation d'outils d'aide au développement de grosses théories dans les systèmes de preuves interactifs. PhD thesis, Conservatoire National des Arts et Métiers, Paris, 1999. [ bib ]
[15] Yves Bertot. Des environnements de programmation aux environnements de preuve, 1999. [ bib ]
[16] Loïc Pottier. Basics notions of algebra. Technical report, Contributions to the Coq system, 1999. [ bib ]
[17] Yves Bertot. The CtCoq system: Design and architecture. Formal Aspects of Computing, 11:225-243, 1999. [ bib ]
[18] J. Harrison and M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of LNCS. Springer-Verlag, 2000. [ bib ]
[19] Hanane Naciri and Laurence Rideau. Affichage interactif, bidimensionnel et incrémental de formules mathématiques. In CARI'2000 5ème Colloque Africain sur la Recherche en Informatique, 2000. [ bib ]
[20] Yann Coscoy. Explication textuelle de preuves pour le calcul des constructions inductives. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2000. [ bib ]
[21] Olivier Pons. Ingéniérie de preuve. In Journées Francophones pour les Langages Applicatifs, January 2000. [ bib ]
[22] Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In Harrison and Aagaard [18], pages 1-16. [ bib ]
[23] Pierre Letouzey and Laurent Théry. Formalizing Stålmarck's algorithm in Coq. In Harrison and Aagaard [18], pages 387-404. [ bib ]
[24] Richard J. Boulton and Paul B. Jackson, editors. Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of LNCS. Springer-Verlag, 2001. [ bib ]
[25] David Pichardie and Yves Bertot. Formalizing convex hull algorithms. In Boulton and Jackson [24], pages 346-361. [ bib ]
[26] Ahmed Amerkad, Yves Bertot, Laurence Rideau, and Loïc Pottier. Mathematics and proof presentation in Pcoq. In PTP'01 Workshop, 2001. [ bib ]
[27] Hanane Naciri and Laurence Rideau. Affichage et manipulation interactive de formules mathématiques dans les documents structurés. Rapport de recherche RR-4140, INRIA, 2001. [ bib | .html ]
[28] Hanane Naciri and Laurence Rideau. The Marriage of MathML ans Theorem Proving. In IACM'2001 Workshop, 2001. [ bib ]
[29] Marc Daumas, Laurence Rideau, and Laurent Théry. A generic library of floating-point numbers and its application to exact computing. In Boulton and Jackson [24], pages 169-184. [ bib ]
[30] Marc Daumas, Claire Moreau-Finot, and Laurent Théry. Computer validated proofs of a toolset for adaptable arithmetic. Research report 4095, INRIA, Le Chesnay, France, 2001. [ bib ]
[31] Nicolas Magaud and Yves Bertot. Changement de représentation des structures de données en coq: le cas des entiers naturels. In Journées Francophones pour les Langages Applicatifs, January 2001. [ bib ]
[32] Laurent Théry. A Machine-Checked Implementation of Buchberger's Algorithm. In Journal of Automated Reasoning, volume 26, pages 107-137, 2001. [ bib ]
[33] Yves Bertot. Formalizing a jvml verifier for initialization in a theorem prover. In Computer Aided Verification (CAV'01), number 2102 in LNCS, Paris, France, July 2001. Springer-Verlag. [ bib ]
[34] Victor A. Carreño, César A. Muñoz, and Sofiène Tahar, editors. Theorem Proving in Higher Order Logics (TPHOLS'02), volume 2410 of LNCS. Springer-Verlag, 2002. [ bib ]
[35] Frédérique Guilhot. Proofs with coq of theorems in plane geometry using oriented angles. Rapport de recherche RR-4356, INRIA, 2002. [ bib ]
[36] Hanane Naciri and Laurence Rideau. FIGUE: Mathematical Formula Layout with Interaction and MathML Support. In Fifth Asian Symposium on Computer Mathematics ASCM'2001, 2002. [ bib ]
[37] Hanane Naciri and Laurence Rideau. Formal Mathematical Proof Explanations in Natural Language Using MathML: An Application to Proofs in Arabic. In MathML International Conference 2002, 2002. [ bib ]
[38] Hanane Naciri and Laurence Rideau. Affichage et diffusion sur internet d'explications en langue arabe de preuves mathématiques. In CARI'2002 6ème Colloque Africain sur la Recherche en Informatique, 2002. [ bib ]
[39] Hanane Naciri. Conception et réalisation d'outils pour l'interaction homme machine dans les environnements de démonstrations mathématiques. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2002. [ bib ]
[40] Antonia Balaa. Fonctions récursives générales dans le calcul des constructions. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2002. [ bib ]
[41] Antonia Balaa and Yves Bertot. Fonctions récursives générales par itération en théorie des types. In Journées Francophones pour les Langages Applicatifs, January 2002. [ bib ]
[42] Assia Mahboubi and Loïc Pottier. Élimination des quantificateurs sur les réels en Coq. In Journées Francophones des Langages Applicatifs, Anglet, Janvier 2002. [ bib ]
[43] Yves Bertot, Nicolas Magaud, and Paul Zimmermann. A proof of GMP square root. Journal of Automated Reasoning, 29:225-252, 2002. [ bib ]
[44] Yves Bertot, Venanzio Capretta, and Kuntal Das Barman. Type-theoretic functional semantics. In Carreño et al. [34]. [ bib ]
[45] David Basin and Burkhart Wolff, editors. Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of LNCS. Springer-Verlag, 2003. [ bib ]
[46] Frédérique Guilhot. Premiers pas vers un cours de géométrie en coq pour le lycée. Rapport de recherche RR-4893, INRIA, 2003. [ bib ]
[47] Laurent Chicli, Loïc Pottier, and Carlos Simpson. Mathematical quotients and quotient types in Coq. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, number 2646 in LNCS, pages 95-107. Springer, 2003. [ bib ]
[48] Sylvie Boldo, Marc Daumas, and Laurent Théry. Formal proofs and computations in finite precision arithmetic. In Calculemus'03, 2003. [ bib ]
[49] Laurent Théry. A Table-Driven Compiler for Pretty Printing. Technical report 0288, INRIA, Le Chesnay, France, 2003. [ bib ]
[50] Nicolas Magaud. Changements de représentation des données dans le calcul des constructions. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2003. [ bib ]
[51] Laurent Chicli. Sur la formalisation des mathématiques dans le Calcul des Constructions Inductives. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2003. [ bib ]
[52] Loïc Pottier. Quelques expériences de calculs et de raisonnements à l'aide de machines, 2003. [ bib ]
[53] Laurent Théry. Proving pearl: Knuth's algorithm for prime numbers. In Basin and Wolff [45]. [ bib ]
[54] Nicolas Magaud. Changing data representation within the coq system. In Basin and Wolff [45]. [ bib ]
[55] Frédérique Guilhot. Formalisation en coq d'un cours de géométrie pour le lycée. In Proceedings of JFLA'04, 2004. [ bib ]
[56] Milad Niqui and Yves Bertot. Qarith: Coq formalisation of lazy rational arithmetic. In S. Berardi, M. Coppo, and F. Damiani, editors, Post-Proceedings of TYPES 2003 Workshop, volume 3085 of LNCS. Springer-Verlag, 2004. [ bib ]
[57] Yves Bertot. Simple canonical representation of rational numbers. In Mathematics, Logic and Computation, volume 85.7 of Electronic Notes in Theoretical Computer Science, 2004. [ bib ]
[58] Philippe Audebaud and Laurence Rideau. TeXmacs as authoring tool for publication and dissemination of formal developments. In User-Interface for Theorem Provers, volume 103, 2004. [ bib ]
[59] Yves Bertot, Frédérique Guilhot, and Loïc Pottier. Visualizing geometrical statements with GeoView. In User-Interfaces for Theorem Provers, volume 103 of Electronic Notes in Theoretical Computer Science, 2004. [ bib ]
[60] Laurent Théry. Colouring proofs: A lightweight approach to adding formal structure to proofs. In User-Interfaces for Theorem Provers, volume 103 of Electronic Notes in Theoretical Computer Science, pages 121-138, 2004. [ bib ]
[61] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004. [ bib ]
[62] Laurent Théry. Formalising Huffman's algorithm. Technical report 034, Università di L'Aquila, L'Aquila, Italie, 2004. [ bib ]
[63] Kuntal Das Barman. Type theoretic semantics for programming languages. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2004. [ bib ]
[64] Yves Bertot. Vérification formelle d'extractions de racines entières. Technical Report RR-5344, INRIA, 2004. à paraitre dans Techniques et Sciences Informatiques, Hermès Science. [ bib ]
[65] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Filliâtre et al. [74], pages 66-81. [ bib ]
[66] Jérôme Creci and Loïc Pottier. La tactique gb. In Journées Francophones des Langages Applicatifs, Anglet, Janvier 2004. [ bib ]
[67] Yves Bertot. Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs. In Proceedings of JFLA'05, 2005. [ bib ]
[68] Laurent Théry. Simplifying polynomial expressions in a proof assistant. Rapport de recherche RR-5614, INRIA, 2005. [ bib | .html ]
[69] Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in coq. In Joe Hurd and Tom Melham, editors, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), LNCS. Springer-Verlag, 2005. [ bib ]
[70] Yves Bertot. Filters on coinductive streams, an application to eratosthenes' sieve. In Typed Lambda Calculi and Applications (TLCA'05), LNCS. Springer, 2005. [ bib ]
[71] Assia Mahboubi. Programming and certifying the cad in the coq system. 2005. 2005 Dagstuhl Seminar on Mathematics, Algorithms and Proofs. [ bib ]
[72] Laurence Rideau and Bernard P. Serpette. Coq à la conquête des moulins. In Journées Francophones pour les Langages Applicatifs, March 2005. [ bib ]
[73] Philippe Audebaud and Christine Paulin. Proofs of randomized algorithms in coq. In Mathematics of Program Construction. LNCS, 2006. [ bib ]
[74] Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors. Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, volume 3839 of LNCS. Springer, 2006. [ bib ]
[75] Assia Mahboubi. Proving formally the implementation of an efficient gcd algorithm for polynomials. In 3rd International Joint Conference on Automated Reasoning (IJCAR), LNCS. Springer, 2006. to appear. [ bib ]
[76] Benjamin Grégoire and Laurent Théry. Certifying large prime numbers: a purely functional library for modular arithmetic. In 3rd International Joint Conference on Automated Reasoning (IJCAR), LNCS. Springer, 2006. to appear. [ bib ]
[77] Benjamin Grégoire, Laurent Théry, and Benjamin Werner. A computational approach to pocklington certificates in type theory. In FLOPS, volume 3945 of LNCS, pages 97-113. Springer, 2006. [ bib ]
[78] Laurent Théry, Pierre Letouzey, and Georges Gonthier. Coq. In The Seventeen Provers of the World, volume 3600 of LNCS, pages 28-35. Springer, 2006. [ bib ]

This file has been generated by bibtex2html 1.83.