[1]  Yves Bertot, Fréderique Guilhot, and Assia Mahboubi. A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science, 21(4):731762, 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 TypeBased Termination.
In Logic for Programming, Artificial Intelligence, and
Reasoning: 17th International Conference, LPAR17, Yogyakarta,
Indonesia, October 1015, 2010, Proceedings 17th International
Conference on Logic for Programming, Artificial Intelligence and
Reasoning, pages 333347, 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. Typebased 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 longterm goal is to extend the Calculus of Inductive Constructions with a typebased 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 8398, Edinburgh RoyaumeUni, 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 coqbased proofs. In Sung Y. Shin, Sascha Ossowski, Michael Schumacher, Mathew J. Palakal, and ChihCheng Hung, editors, Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 2226, 2010, pages 12681269. ACM, March 2010. [ bib ] 
[8] 
Ioana Pasca.
Formal Proofs for Theoretical Properties of Newton's
Method.
Research Report RR7228, 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]  TuanMinh Pham and Yves Bertot. A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. In UITP'10, UserInterfaces 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 1114, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 115130. Springer, 2010. [ bib  http ] 
[12]  Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, and Sylvain Heraud. A machinechecked formalization of sigmaprotocols. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 1719, 2010, pages 246260. IEEE Computer Society, 2010. [ bib  http ] 
[13]  JeanFranç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 1114, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 211226. 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 510, 2010. Proceedings, volume 6167 of Lecture Notes in Computer Science, pages 219233. 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 6976. IEEE, September 2009. [ bib ] 
[16] 
Clément Hurlin.
Specification and Verification of Multithreaded ObjectOriented 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.

[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 408423. 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
5268. SpringerVerlag, 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 438452. 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
objectoriented 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 SophiaAntipolis  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 587592. 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 3248. 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 codebased cryptographic proofs. In 36th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 90101. 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 541560, 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, JeanJacques 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 337361. 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 153194. 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 220236. 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 Javalike 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 1216. Springer, August 2008. [ bib  http ] 
[36]  Laurent Théry. Proof Pearl. Revisiting the MiniRubik 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 1821, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 1216. 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 173181. 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):307326, 2008.
[ bib 
.pdf ]
This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semanticallyequivalent 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 8996, New York, NY, USA, 2008. ACM. [ bib  DOI  http ] 
[43]  Nicolas Julien. Certified exact real arithmetic using coinduction 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 CayleyHamilton. 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 86101. SpringerVerlag, 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 319333. SpringerVerlag, 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, coinduction et base arbitraire. In Journées francophones pour les langages applicatifs, JFLA'07, 2007. [ bib  http ] 
[53]  Yves Bertot. Affine functions and series with coinductive real numbers. Mathematical Structure in Computer Sciences, 17(1):3763, 2007. [ bib  http ] 
[54]  Assia Mahboubi. Implementing the cylindrical algebraic decomposition within the coq system. Mathematical Structure in Computer Sciences, 17(1):99127, 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 fixpoint 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 NiceSophia 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 2835. 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 97113. 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 423437. SpringerVerlag, 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 438452. SpringerVerlag, 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]  JeanChristophe Filliâtre, Christine PaulinMohring, and Benjamin Werner, editors. Types for Proofs and Programs, International Workshop, TYPES 2004, JouyenJosas, France, December 1518, 2004, Revised Selected Papers, volume 3839 of LNCS. Springer, 2006. [ bib ] 
[67]  Thierry Coquand, Henri Lombardi, and MarieFranç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):11611185, 2005. paru également comme rapport de recherche INRIA RR5344. [ 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. SpringerVerlag, 2005. [ bib ] 
[74]  Laurent Théry. Simplifying polynomial expressions in a proof assistant. Rapport de recherche RR5614, INRIA, 2005. [ bib  .html ] 
[75]  Yves Bertot. Calcul de formules affines et de séries entières en arithmétique exacte avec types coinductifs. 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 6681. [ bib ] 
[77]  Kuntal Das Barman. Type theoretic semantics for programming languages. PhD thesis, Université de NiceSophia 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. SpringerVerlag, 2004. [ bib ] 
[80]  Laurent Théry. Colouring proofs: A lightweight approach to adding formal structure to proofs. In UserInterfaces for Theorem Provers, volume 103 of Electronic Notes in Theoretical Computer Science, pages 121138, 2004. [ bib ] 
[81]  Yves Bertot, Frédérique Guilhot, and Loïc Pottier. Visualizing geometrical statements with GeoView. In UserInterfaces 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 UserInterface 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, PostProceedings of TYPES 2003 Workshop, volume 3085 of LNCS. SpringerVerlag, 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 NiceSophia Antipolis, Nice, 2003. [ bib ] 
[90]  Laurent Chicli. Sur la formalisation des mathématiques dans le Calcul des Constructions Inductives. PhD thesis, Université de NiceSophia Antipolis, Nice, 2003. [ bib ] 
[91]  Nicolas Magaud. Changements de représentation des données dans le calcul des constructions. PhD thesis, Université de NiceSophia Antipolis, Nice, 2003. [ bib ] 
[92]  Laurent Théry. A TableDriven 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 95107. 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 RR4893, 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. SpringerVerlag, 2003. [ bib ] 
[97]  Yves Bertot, Venanzio Capretta, and Kuntal Das Barman. Typetheoretic 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:225252, 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 NiceSophia 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 NiceSophia 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 RR4356, 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. SpringerVerlag, 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. SpringerVerlag. [ bib ] 
[109]  Laurent Théry. A MachineChecked Implementation of Buchberger's Algorithm. In Journal of Automated Reasoning, volume 26, pages 107137, 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 MoreauFinot, 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 floatingpoint numbers and its application to exact computing. In Boulton and Jackson [117], pages 169184. [ 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 RR4140, 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 346361. [ 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. SpringerVerlag, 2001. [ bib ] 
[118]  Pierre Letouzey and Laurent Théry. Formalizing Stålmarck's algorithm in Coq. In Harrison and Aagaard [123], pages 387404. [ bib ] 
[119]  Antonia Balaa and Yves Bertot. Fixpoint equations for wellfounded recursion in type theory. In Harrison and Aagaard [123], pages 116. [ 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 NiceSophia 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. SpringerVerlag, 2000. [ bib ] 
[124]  Yves Bertot. The CtCoq system: Design and architecture. Formal Aspects of Computing, 11:225243, 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 NiceSophia 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:161194, 1998. [ bib ] 
[130]  Laurent Théry. A certified version of Buchberger's algorithm. In Automated DeductionCADE15, volume 1421 of Lecture Notes in Artificial Intelligence, pages 349364. SpringerVerlag, 1998. [ bib ] 
[131]  Yves Bertot. A certified compiler for an imperative language. Research report RR3488, INRIA, 1998. [ bib ] 
[132]  John Harrison and Laurent Théry. A skeptic's approach to combining hol and maple. J. Autom. Reasoning, 21(3):279294, 1998. [ bib ] 
[133]  Laurence Rideau and Laurent Théry. Interactive programming environment for ml. Rapport de recherche RR3139, INRIA, 1997. [ bib  .html ] 
[134]  Yves Bertot. Direct manipulation of algebraic formulae in interactive proof systems. In UserInterfaces for theorem provers (UITP'97), 1997. [ bib  .html ] 
[135]  Yves Bertot. Headtactics simplification. In Johnson [136], pages 1629. [ bib ] 
[136]  Michael Johnson, editor. Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 1317, 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 231234. [ bib ] 
[138]  Michael A. McRobbie and John K. Slaney, editors. Automated Deduction  CADE13, 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 531545, 1995. [ bib ] 
[140]  Yann Coscoy, Gilles Kahn, and Laurent Théry. Extracting text from proofs. In TLCA, volume 902 of LNCS, pages 109123, 1995. [ bib ] 
[141]  Mariangiola DezaniCiancaglini and Gordon D. Plotkin, editors. Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 1012, 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 141160, 1994. [ bib ] 
[143]  Laurent Théry, Yves Bertot, and Gilles Kahn. Real Theorem Provers Deserve Real UserInterfaces. Software Engineering Notes, 17(5), 1992. Proceedings of the 5th Symposium on Software Development Environments. [ bib ] 
[144]  Yves Bertot. Origin functions in lambdacalculus and term rewriting systems. In CAAP '92: Proceedings of the 17th Colloquium on Trees in Algebra and Programming, volume 581, pages 4965, London, UK, 1992. SpringerVerlag. [ 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 327337, 1991. [ bib  .html ] 
[147]  Yves Bertot. Implementation of an interpreter for a parallel language in centaur. In European Symposium on Programming, volume 432, pages 5769. Springer, 1990. [ bib ] 
This file was generated by bibtex2html 1.96.