Marelle Bibliography

[1] Yves Bertot, Fréderique Guilhot, and Assia Mahboubi. A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science, 21(4):731-762, 2011. [ bib | DOI | http ]
[2] Ioana Pasca. Formal Verification for Numerical Methods. PhD thesis, Université Nice - Sophia Antipolis, November 2010. [ bib | http ]
[3] Benjamin Grégoire and Jorge Sacchini. On Strong Normalization of the Calculus of Constructions with Type-Based Termination. In Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pages 333-347, Yogyakarta Indonésie, November 2010. The original publication is available at www.springerlink.com. [ bib | DOI | http ]
Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-based termination is a mechanism for ensuring termination that uses types annotated with size information to check that recursive calls are performed on smaller arguments. Our long-term goal is to extend the Calculus of Inductive Constructions with a type-based termination mechanism and prove its logical consistency. In this paper, we present an extension of the Calculus of Constructions (including universes and impredicativity) with sized natural numbers, and prove strong normalization and logical consistency. Moreover, the proof can be easily adapted to include other inductive types.

[4] Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry. Extending Coq with Imperative Features and its Application to SAT Verification. In Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 83-98, Edinburgh Royaume-Uni, July 2010. Springer. [ bib | http ]
[5] Yves Bertot, editor. Second Coq Workshop, July 2010. [ bib | http ]
[6] Yves Bertot, Fréderique Guilhot, and Assia Mahboubi. A formal study of Bernstein coefficients and polynomials. Technical report, INRIA, July 2010. [ bib | http ]
[7] Tuan Minh Pham. Similar triangles and orientation in plane elementary geometry for coq-based proofs. In Sung Y. Shin, Sascha Ossowski, Michael Schumacher, Mathew J. Palakal, and Chih-Cheng Hung, editors, Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22-26, 2010, pages 1268-1269. ACM, March 2010. [ bib ]
[8] Ioana Pasca. Formal Proofs for Theoretical Properties of Newton's Method. Research Report RR-7228, INRIA, March 2010. [ bib | http ]
We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suite the features of a proof assistant, and designing new proofs based on the existing ones to deal with optimizations of the method. We start from Kantorovitch's theorem that states the convergence of Newton's method in the case of a system of equations. To formalize this proof inside the proof assistant Coq we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.

Keywords: proof assistants ; formalization of mathematics ; multivariate analysis ; Kantorovitch's theorem ; Newton's method with rounding
[9] Tuan-Minh Pham and Yves Bertot. A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. In UITP'10, User-Interfaces for Theorem Provers, 2010. [ bib ]
[10] Benjamin Grégoire, Loïc Pottier, and Laurent Théry. Proof certificates for algebra and their application to automatic geometry theorem proving. Lecture Notes in Artificial Intelligence, 2010. [ bib | http ]
[11] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Programming language techniques for cryptographic proofs. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 115-130. Springer, 2010. [ bib | http ]
[12] Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, and Sylvain Heraud. A machine-checked formalization of sigma-protocols. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 246-260. IEEE Computer Society, 2010. [ bib | http ]
[13] Jean-François Dufourd and Yves Bertot. Formal study of plane delaunay triangulation. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 211-226. Springer, 2010. [ bib | http ]
[14] Ioana Pasca. Formally verified conditions for regularity of interval matrices. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings, volume 6167 of Lecture Notes in Computer Science, pages 219-233. Springer, 2010. [ bib | http ]
[15] Maxime Dénès, Benjamin Lesage, Yves Bertot, and Adrien Richard. Formal proof of theorems on genetic regulatory networks. In Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2009), pages 69-76. IEEE, September 2009. [ bib ]
[16] Clément Hurlin. Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis, Université Nice - Sophia Antipolis, September 2009. [ bib ]
First, we develop verification rules in separation logic for primi tives concerning multithreading: the primitives fork and join that control how threads start and how threads wait, and the primitive for reentrant locks (locks that can be acquired and released more than once) that are used in Java.

Second, we develop three analyses that use separation logic. The first analysis permits to specify sequences of method calls and to verify that they are correct w.r.t. method contracts. The second analysis presents a fast algorithm to disprove entailment between separation logic formulae. The third analysis shows how to parallelize a nd optimize programs by rewriting their proofs.

[17] Nicolas Julien and Ioana Pasca. Formal Verification of Exact Computations Using Newton's Method. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of LNCS, pages 408-423. Springer, August 2009. [ bib | http ]
[18] Clément Hurlin. Automatic parallelization and optimization of programs by proof rewriting (or automatic parallelization with separation logic!). In Static Analysis Symposium (SA S'09), volume 5673 of Lecture Notes in Computer Science, pages 52-68. Springer-Verlag, August 2009. [ bib | DOI | .pdf ]
We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its pr oof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating pr oof trees and a rewrite system on proof trees.

[19] Sidi Ould Biha. Finite groups representation theory with coq. In Mathematical Knowledge Management, volume 5625 of LNAI, pages 438-452. Springer, July 2009. [ bib | http ]
[20] Clément Hurlin, François Bobot, and Alexander J. Summers. Size does matter : Two certified abstractions to disprove entailment in intuitionistic and classical separation logic. In International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), July 2009.bib | .pdf | .dvi | .ps ]
We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A does not entail B. We provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).

[21] Clément Hurlin. Automatic parallelization and optimization of programs by proof rewriting (or automatic parallelization with separation logic!). Technical Report 6806, INRIA Sophia-Antipolis - Méditerrannée, June 2009. [ bib ]
[22] Clément Hurlin. Specifying and checking protocols of multithreaded classes. In ACM Symposium on Applied Computing (SAC'09), Software Verification and Testing Track, pages 587-592. ACM, March 2009. Additional material (examples, detailed statistics, and implementation) is available: pyrolobus. [ bib | DOI | .pdf ]
In the Design By Contract (DBC) approach, programmers specify methods with pre and postconditions (also called contracts). Earlier work added protocols to the DBC approach to describe allowed method call sequences for classes. We extend this work to We present the semantical foundations of our extension. We describe a new technique to check that method contracts are correct w.r.t. to protocols. We show how to generate programs that must be proven to show that method contracts are correct w.r.t. to protocols. Because little support currently exists to help writing method contracts, our technique helps programmers to check their contracts early in the development process.

[23] Maxime Dénès, Benjamin Lesage, Yves Bertot, and Adrien Richard. Formal proof of theorems on genetic regulatory networks. In SYNASC'09 Synasc 2009, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara Roumanie, 2009. IEEE. [ bib | http ]
We describe the formal verification of two theorems of theoretical biology. These theorems concern genetic regulatory networks: they give, in a discrete modeling framework, relations between the topology and the dynamics of these biological networks. In the considered discrete modeling framework, the dynamics is described by a transition graph, where vertices are vectors indicating the expression level of each gene, and where edges represent the evolution of these expression levels. The topology is also described by a graph, called interaction graph, where vertices are genes and where edges correspond to influences between genes. The two results we formalize show that circuits of some kind must be present in the interaction graph if some behaviors are possible in the transition graph. This work was performed with the ssreflect extension of the Coq system.

[24] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging Mathematical Structures. In Tobias Nipkow and Christian Urban, editors, Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, Munich Allemagne, 2009. Springer. G.: Mathematics of Computing/G.4: MATHEMATICAL SOFTWARE, I.: Computing Methodologies/I.1: SYMBOLIC AND ALGEBRAIC MANIPULATION/I.1.0: General. [ bib | http ]
Keywords: Formalization of Algebra, Coercive subtyping, Type inference, Coq, SSReflect
[25] Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, and Jorge Luis Sacchini. A new elimination rule for the Calculus of Inductive Constructions. In S. Berardi, F. Damiani, and U de'Liguoro, editors, Types for proofs and programs 2008, volume 5497 of Lecture Notes in Computer Science, pages 32-48. Springer, 2009. [ bib ]
[26] Gilles Barthe, Benjamin Grégoire, Federico Olmedo, and Santiago Zanella Béguelin. Formally certifying the security of digital signature schemes. In 30th IEEE Symposium on Security and Privacy, S&P 2009. IEEE, 2009. [ bib ]
[27] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 90-101. ACM, 2009. [ bib | http ]
[28] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Cesar Kunz, and Anne Pacalet. Implementing a direct method for certificate translation. In International Conference on Formal Engineering Methods, ICFEM 2009, number 5885 in Lectures Notes in Computer Science, pages 541-560, 2009. [ bib ]
[29] Jan Olaf Blech and Benjamin Grégoire. Using checker predicates in certifying code generation. In Proceedings of the Workshop Compiler Optimization meets Compiler Verification (COCV 2009). ENTCS, 2009. To appear. [ bib ]
[30] Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin, editors. From Semantics to Computer Science, essays in Honour of Gilles Kahn. Cambridge University Press, 2009. [ bib ]
[31] Yves Bertot. From Semantics to Computer Science, essays in Honour of Gilles Kahn, chapter Theorem proving support in programming language semantics, pages 337-361. In Bertot et al. [30], 2009. [ bib | http ]
[32] Yves Bertot. Structural abstract interpretation, a formal study in coq. In A. Bove, L. S. Barbosa, A. Pardo, and J. S. Pinto, editors, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, revised tutorial lectures, volume 5520 of Lecture Notes in Computer Science, pages 153-194. Springer, 2009. [ bib | http ]
[33] Yves Bertot and Ekaterina Komendantskaya. Using structural recursion for corecursion. In S. Berardi, F. Damiani, and U de'Liguoro, editors, Types for proofs and programs 2008, volume 5497 of Lecture Notes in Computer Science, pages 220-236. Springer, 2009. [ bib | http ]
[34] Christian Haack and Clément Hurlin. Resource usage protocols for iterators. Journal of Object Technology, 8(4), 2009. This is an extended version of a paper that appeared in the IWACO'08 workshop. [ bib | .html ]
We discuss usage protocols for iterator objects that prevent concurrent modifications of the underlying collection while iterators are in progress. We formalize these protocols in Java-like object interfaces, enriched with separation logic contracts. We present examples of iterator clients and proofs that they adhere to the iterator protocol, as well as examples of iterator implementations and proofs that they implement the iterator interface.

[35] Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. Canonical Big Operators. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of Lecture Notes in Computer Science, pages 12-16. Springer, August 2008. [ bib | http ]
[36] Laurent Théry. Proof Pearl. Revisiting the Mini-Rubik in Coq. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS, August 2008. [ bib ]
[37] Yves Bertot and Ekaterina Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq. In Proceedings of CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science, volume 203 of ENTCS, pages 25 - 47, April 2008. [ bib | http ]
[38] Yves Bertot. A short presentation of coq. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 12-16. Springer, 2008. [ bib ]
[39] Loïc Pottier. Connecting gröbner bases programs with coq to do proofs in algebra, geometry and arithmetics. In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz, editors, Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, number 418 in CEUR Workshop Proceedings, 2008. [ bib ]
[40] Yves Bertot and Laurent Théry. Dependent types, theorem proving, and applications for a verifying compiler. In 1st IFIP TC 2/WG 2.3 Conference, on Verified Software: Theories, Tools, Experiments (VSTTE), volume 4171 of LNCS, pages 173-181. Springer, 2008. [ bib ]
[41] Laurence Rideau, Bernard P. Serpette, and Xavier Leroy. Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 40(4):307-326, 2008. [ bib | .pdf ]
This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.

[42] Yves Bertot and Vladimir Komendantsky. Fixed point semantics and partial recursion in coq. In PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, pages 89-96, New York, NY, USA, 2008. ACM. [ bib | DOI | http ]
[43] Nicolas Julien. Certified exact real arithmetic using co-induction in arbitrary integer base. In Functional and Logic Programming Symposium (FLOPS), Lecture Notes in Computer Science. Springer, 2008. [ bib | http ]
[44] Sidi Ould Biha. Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton. In Journées Francophones des Langages Applicatifs, January 2008. [ bib | http ]
[45] Ioana Pasca. A Formal Verification for Kantorovitch's Theorem. In Journées Francophones des Langages Applicatifs, January 2008. [ bib | http ]
[46] Cody Roux. Types, Logique et Coercions Implicites. In Journées Francophones des Langages Applicatifs, January 2008. [ bib | http ]
[47] Yves Bertot and Vladimir Komendantsky. Fixed point semantics and partial recursion in coq. Technical report, INRIA, November 2007. Draft paper, submitted to a conference. [ bib | http ]
[48] Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, and Laurent Théry. A modular formalisation of finite group theory. In Klaus Schneider and Jens Brandt, editors, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of LNCS, pages 86-101. Springer-Verlag, September 2007. [ bib | http ]
[49] Laurent Théry and Guillaume Hanrot. Primality proving with elliptic curves. In Klaus Schneider and Jens Brandt, editors, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of LNCS, pages 319-333. Springer-Verlag, September 2007. [ bib | http ]
[50] Laurence Rideau, Bernard P. Serpette, and Xavier Leroy. Battling windmills with coq: formal verification of a compilation algorithm for parallel moves. Technical report, INRIA, September 2007. Draft paper, submitted to a journal. [ bib | http ]
[51] Jérémy Blanc, J.P. Giacometti, André Hirschowitz, and Loïc Pottier. Proofs for freshmen with coqweb. In H. Geuvers and P. Courtieu, editors, Proceedings of the International Workshop on Proof Assistants and Types in Education, June 25th, 2007, associated workshop of the 2007 Federated Conference on Rewriting, Deduction and Programming, CNAM Paris, France, June 2007. [ bib | .pdf ]
[52] Nicolas Julien. Arithmétique réelle exacte certifiée, co-induction et base arbitraire. In Journées francophones pour les langages applicatifs, JFLA'07, 2007. [ bib | http ]
[53] Yves Bertot. Affine functions and series with co-inductive real numbers. Mathematical Structure in Computer Sciences, 17(1):37-63, 2007. [ bib | http ]
[54] Assia Mahboubi. Implementing the cylindrical algebraic decomposition within the coq system. Mathematical Structure in Computer Sciences, 17(1):99-127, 2007. [ bib ]
[55] Yves Bertot. Theorem proving support in programming language semantics. Technical Report 6242, INRIA, 2007. [ bib | http ]
[56] Loïc Pottier. Ambiguous typing. Technical report, INRIA, December 2006. [ bib | http ]
[57] Laurent Théry and Laurence Rideau. Formalising sylow's theorems in coq. Technical Report 0327, INRIA, November 2006. [ bib | http ]
[58] Yves Bertot. Extending the calculus of constructions with tarski's fix-point theorem. Technical report, INRIA, October 2006. [ bib | http ]
[59] Assia Mahboubi. Contribution à la certification des calculs dans R : théorie, preuves, programmation. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2006. [ bib ]
[60] 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 ]
[61] Benjamin Grégoire, Laurent Théry, and Benjamin Werner. A computational approach to pocklington certificates in type theory. In Functional and Logic Programming Symposium (FLOPS), volume 3945 of LNCS, pages 97-113. Springer, 2006. [ bib ]
[62] Benjamin Grégoire and Laurent Théry. A purely functional library for modular arithmetic and its application for certifying large prime numbers. In U. Furbach and N. Shankar, editors, 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of Lecture Notes in Artificial Intelligence, pages 423-437. Springer-Verlag, 2006. [ bib ]
[63] Assia Mahboubi. Proving formally the implementation of an efficient gcd algorithm for polynomials. In U. Furbach and N. Shankar, editors, 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of Lecture Notes in Artificial Intelligence, pages 438-452. Springer-Verlag, 2006. [ bib | http ]
[64] Nicolas Julien. Vérification formelle d'arithmétique réelle exacte et fonctions analytiques, 2006. [ bib ]
[65] Sidi Ould Biha. Vérification d'un algorithme de test de primalité avec caduceus, 2006. [ bib ]
[66] 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 ]
[67] Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors. Mathematics, Algorithms, Proofs, 9.-14. January 2005, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2006. [ bib ]
[68] Philippe Audebaud and Christine Paulin. Proofs of randomized algorithms in coq. In Tarmo Uustalu, editor, Mathematics of Program Construction, number 4014. LNCS, 2006. [ bib ]
[69] Laurence Rideau and Bernard P. Serpette. Coq à la conquête des moulins. In Journées Francophones pour les Langages Applicatifs, March 2005. [ bib ]
[70] Assia Mahboubi. Programming and certifying a cad algorithm in the coq system. In Coquand et al. [67]. [ bib ]
[71] Yves Bertot. Filters on coinductive streams, an application to eratosthenes' sieve. In Typed Lambda Calculi and Applications (TLCA'05), LNCS. Springer, 2005. [ bib ]
[72] Yves Bertot. Vérification formelle d'extractions de racines entières. Techniques et Sciences Informatiques, 24(9):1161-1185, 2005. paru également comme rapport de recherche INRIA RR-5344. [ bib | http ]
[73] 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 ]
[74] Laurent Théry. Simplifying polynomial expressions in a proof assistant. Rapport de recherche RR-5614, INRIA, 2005. [ bib | .html ]
[75] 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 ]
[76] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Filliâtre et al. [66], pages 66-81. [ bib ]
[77] Kuntal Das Barman. Type theoretic semantics for programming languages. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2004. [ bib ]
[78] Laurent Théry. Formalising Huffman's algorithm. Technical report 034, Università di L'Aquila, L'Aquila, Italie, 2004. [ bib ]
[79] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004. [ bib ]
[80] 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 ]
[81] 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 ]
[82] 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 ]
[83] 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 ]
[84] 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 ]
[85] 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 ]
[86] Yves Bertot and Pierre Castéran. Coq'Art: examples and exercises, 2004. http://www.labri.fr/Perso/~casteran/CoqArt. [ bib ]
[87] Nicolas Magaud. Changing data representation within the coq system. In Basin and Wolff [96]. [ bib ]
[88] Laurent Théry. Proving pearl: Knuth's algorithm for prime numbers. In Basin and Wolff [96]. [ bib ]
[89] Loïc Pottier. Quelques expériences de calculs et de raisonnements à l'aide de machines. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2003. [ bib ]
[90] Laurent Chicli. Sur la formalisation des mathématiques dans le Calcul des Constructions Inductives. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2003. [ bib ]
[91] Nicolas Magaud. Changements de représentation des données dans le calcul des constructions. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2003. [ bib ]
[92] Laurent Théry. A Table-Driven Compiler for Pretty Printing. Technical report 0288, INRIA, Le Chesnay, France, 2003. [ bib ]
[93] Sylvie Boldo, Marc Daumas, and Laurent Théry. Formal proofs and computations in finite precision arithmetic. In Calculemus'03, 2003. [ bib ]
[94] 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 ]
[95] 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 ]
[96] 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 ]
[97] Yves Bertot, Venanzio Capretta, and Kuntal Das Barman. Type-theoretic functional semantics. In Carreño et al. [107]. [ bib ]
[98] Yves Bertot, Nicolas Magaud, and Paul Zimmermann. A proof of GMP square root. Journal of Automated Reasoning, 29:225-252, 2002. [ bib ]
[99] Assia Mahboubi and Loïc Pottier. Élimination des quantificateurs sur les réels en Coq. In Journées Francophones des Langages Applicatifs, Anglet, January 2002. [ bib ]
[100] 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 ]
[101] Antonia Balaa. Fonctions récursives générales dans le calcul des constructions. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2002. [ bib ]
[102] 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 ]
[103] 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 ]
[104] 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 ]
[105] 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 ]
[106] Frédérique Guilhot. Proofs with coq of theorems in plane geometry using oriented angles. Rapport de recherche RR-4356, INRIA, 2002. [ bib ]
[107] 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 ]
[108] 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 ]
[109] Laurent Théry. A Machine-Checked Implementation of Buchberger's Algorithm. In Journal of Automated Reasoning, volume 26, pages 107-137, 2001. [ bib ]
[110] 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 ]
[111] 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 ]
[112] 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 [117], pages 169-184. [ bib ]
[113] Hanane Naciri and Laurence Rideau. The Marriage of MathML ans Theorem Proving. In IACM'2001 Workshop, 2001. [ bib ]
[114] 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 ]
[115] Ahmed Amerkad, Yves Bertot, Laurence Rideau, and Loïc Pottier. Mathematics and proof presentation in Pcoq. In PTP'01 Workshop, 2001. [ bib ]
[116] David Pichardie and Yves Bertot. Formalizing convex hull algorithms. In Boulton and Jackson [117], pages 346-361. [ bib ]
[117] 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 ]
[118] Pierre Letouzey and Laurent Théry. Formalizing Stålmarck's algorithm in Coq. In Harrison and Aagaard [123], pages 387-404. [ bib ]
[119] Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In Harrison and Aagaard [123], pages 1-16. [ bib ]
[120] Olivier Pons. Ingéniérie de preuve. In Journées Francophones pour les Langages Applicatifs, January 2000. [ bib ]
[121] Yann Coscoy. Explication textuelle de preuves pour le calcul des constructions inductives. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 2000. [ bib ]
[122] 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 ]
[123] 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 ]
[124] Yves Bertot. The CtCoq system: Design and architecture. Formal Aspects of Computing, 11:225-243, 1999. [ bib ]
[125] Loïc Pottier. Basics notions of algebra. Technical report, Contributions to the Coq system, 1999. [ bib ]
[126] Yves Bertot. Des environnements de programmation aux environnements de preuve. PhD thesis, Université de Nice-Sophia Antipolis, Nice, 1999. [ bib ]
[127] 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 ]
[128] 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 ]
[129] 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 ]
[130] 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 ]
[131] Yves Bertot. A certified compiler for an imperative language. Research report RR-3488, INRIA, 1998. [ bib ]
[132] John Harrison and Laurent Théry. A skeptic's approach to combining hol and maple. J. Autom. Reasoning, 21(3):279-294, 1998. [ bib ]
[133] Laurence Rideau and Laurent Théry. Interactive programming environment for ml. Rapport de recherche RR-3139, INRIA, 1997. [ bib | .html ]
[134] Yves Bertot. Direct manipulation of algebraic formulae in interactive proof systems. In User-Interfaces for theorem provers (UITP'97), 1997. [ bib | .html ]
[135] Yves Bertot. Head-tactics simplification. In Johnson [136], pages 16-29. [ bib ]
[136] Michael Johnson, editor. Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 13-17, 1997, Proceedings, volume 1349 of Lecture Notes in Computer Science. Springer, 1997. [ bib ]
[137] Janet Bertot and Yves Bertot. Ctcoq: A system presentation. In McRobbie and Slaney [138], pages 231-234. [ bib ]
[138] Michael A. McRobbie and John K. Slaney, editors. Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, volume 1104 of Lecture Notes in Computer Science. Springer, 1996. [ bib ]
[139] 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 ]
[140] Yann Coscoy, Gilles Kahn, and Laurent Théry. Extracting text from proofs. In TLCA, volume 902 of LNCS, pages 109-123, 1995. [ bib ]
[141] 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, 1995. [ bib ]
[142] 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 ]
[143] 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 ]
[144] Yves Bertot. Origin functions in lambda-calculus and term rewriting systems. In CAAP '92: Proceedings of the 17th Colloquium on Trees in Algebra and Programming, volume 581, pages 49-65, London, UK, 1992. Springer-Verlag. [ bib ]
[145] Yves Bertot. A Canonical Calculus of Residuals. In G. Huet and G. Plotkin, editors, Proceedings of the 2nd workshop on Logical Frameworks. Cambridge University Press, 1992. [ bib | .html ]
[146] Y. Bertot. Occurrences in debugger specifications. In Proceedings of the ACM SIGPLAN '91 Conference on Programming Language Design and Implementation (PLDI), volume 26, pages 327-337, 1991. [ bib | .html ]
[147] Yves Bertot. Implementation of an interpreter for a parallel language in centaur. In European Symposium on Programming, volume 432, pages 57-69. Springer, 1990. [ bib ]

This file was generated by bibtex2html 1.96.