References

[1]
David Aspinall. Proof general. http://proofgeneral.inf.ed.ac.uk/.
[2]
Ph. Audebaud. Partial Objects in the Calculus of Constructions. In Proceedings of the sixth Conf. on Logic in Computer Science. IEEE, 1991.
[3]
Ph. Audebaud. CC+ : an extension of the Calculus of Constructions with fixpoints. In B. Nordström and K. Petersson and G. Plotkin, editor, Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 21–34, 1992. Also Research Report LIP-ENS-Lyon.
[4]
Ph. Audebaud. Extension du Calcul des Constructions par Points fixes. PhD thesis, Université Bordeaux I, 1992.
[5]
L. Augustsson. Compiling Pattern Matching. In Conference Functional Programming and Computer Architecture, 1985.
[6]
H. Barendregt. Lambda Calculi with Types. Technical Report 91-19, Catholic University Nijmegen, 1991. In Handbook of Logic in Computer Science, Vol II.
[7]
H. Barendregt and T. Nipkow, editors. Types for Proofs and Programs, volume 806 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 1994.
[8]
H.P. Barendregt. The Lambda Calculus its Syntax and Semantics. North-Holland, 1981.
[9]
B. Barras. Auto-validation d’un système de preuves avec familles inductives. Thèse de doctorat, Université Paris 7, 1999.
[10]
J.L. Bates and R.L. Constable. Proofs as Programs. ACM transactions on Programming Languages and Systems, 7, 1985.
[11]
M.J. Beeson. Foundations of Constructive Mathematics, Metamathematical Studies. Sprin­ger-Verlag, 1985.
[12]
G. Bellin and J. Ketonen. A decision procedure revisited : Notes on direct logic, linear logic and its implementation. Theoretical Computer Science, 95:115–142, 1992.
[13]
Stefano Berardi and Mario Coppo, editors. Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science. Springer, 1996.
[14]
Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS series. Springer Verlag, 2004.
[15]
E. Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967.
[16]
S. Boutin. Certification d’un compilateur ML en Coq. Master’s thesis, Université Paris 7, September 1992.
[17]
S. Boutin. Réflexions sur les quotients. thèse d’université, Paris 7, April 1997.
[18]
S. Boutin. Using reflection to build efficient and certified decision procedure s. In Martin Abadi and Takahashi Ito, editors, TACS’97, volume 1281 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 1997.
[19]
R.S. Boyer and J.S. Moore. A computational logic. ACM Monograph. Academic Press, 1979.
[20]
Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors. Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, volume 2277 of Lecture Notes in Computer Science. Springer, 2002.
[21]
Laurent Chicli, Loïc Pottier, and Carlos Simpson. Mathematical quotients and quotient types in coq. In Geuvers and Wiedijk [64].
[22]
R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
[23]
Th. Coquand. Une Théorie des Constructions. PhD thesis, Université Paris 7, January 1985.
[24]
Th. Coquand. An Analysis of Girard’s Paradox. In Symposium on Logic in Computer Science, Cambridge, MA, 1986. IEEE Computer Society Press.
[25]
Th. Coquand. Metamathematical Investigations of a Calculus of Constructions. In P. Oddifredi, editor, Logic and Computer Science. Academic Press, 1990. INRIA Research Report 1088, also in [62].
[26]
Th. Coquand. A New Paradox in Type Theory. In Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science, August 1991.
[27]
Th. Coquand. Pattern Matching with Dependent Types. In Nordström et al. [107].
[28]
Th. Coquand. Infinite Objects in Type Theory. In Barendregt and Nipkow [7].
[29]
Th. Coquand and G. Huet. Constructions : A Higher Order Proof System for Mechanizing Mathematics. In EUROCAL’85, volume 203 of Lecture Notes in Computer Science, Linz, 1985. Sprin­ger-Verlag.
[30]
Th. Coquand and G. Huet. Concepts Mathématiques et Informatiques formalisés dans le Calcul des Constructions. In The Paris Logic Group, editor, Logic Colloquium’85. North-Holland, 1987.
[31]
Th. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2/3), 1988.
[32]
Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog’88, volume 417 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 1990.
[33]
P. Corbineau. A declarative language for the coq proof assistant. In M. Miculan, I. Scagnetto, and F. Honsell, editors, TYPES ’07, Cividale del Friuli, Revised Selected Papers, volume 4941 of Lecture Notes in Computer Science, pages 69–84. Springer, 2007.
[34]
C. Cornes. Conception d’un langage de haut niveau de représentation de preuves. Thèse de doctorat, Université Paris 7, November 1997.
[35]
Cristina Cornes and Delphine Terrasse. Automating inversion of inductive predicates in coq. In Berardi and Coppo [13], pages 85–104.
[36]
J. Courant. Explicitation de preuves par récurrence implicite. Master’s thesis, DEA d’Informatique, ENS Lyon, September 1994.
[37]
N.J. de Bruijn. Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indag. Math., 34, 1972.
[38]
N.J. de Bruijn. A survey of the project Automath. In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
[39]
D. de Rauglaudre. Camlp4 version 1.07.2. In Camlp4 distribution, 1998.
[40]
D. Delahaye. Information retrieval in a coq proof library using type isomorphisms. In Proceedings of TYPES ’99, Lökeberg, Lecture Notes in Computer Science. Sprin­ger-Verlag, 1999.
[41]
D. Delahaye. A Tactic Language for the System Coq. In Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island, volume 1955 of Lecture Notes in Computer Science, pages 85–95. Sprin­ger-Verlag, November 2000.
[42]
D. Delahaye and M. Mayero. Field: une procédure de décision pour les nombres réels en Coq. In Journées Francophones des Langages Applicatifs, Pontarlier. INRIA, Janvier 2001.
[43]
R. di Cosmo. Isomorphisms of Types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. ISBN-0-8176-3763-X.
[44]
G. Dowek. Naming and scoping in a mathematical vernacular. Research Report 1283, INRIA, 1990.
[45]
G. Dowek. Démonstration automatique dans le Calcul des Constructions. PhD thesis, Université Paris 7, December 1991.
[46]
G. Dowek. L’indécidabilité du filtrage du troisième ordre dans les calculs avec types dépendants ou constructeurs de types. Compte-Rendus de l’Académie des Sciences, I, 312(12):951–956, 1991. The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors.
[47]
G. Dowek. A second order pattern matching algorithm in the cube of typed λ-calculi. In Proceedings of Mathematical Foundation of Computer Science, volume 520 of Lecture Notes in Computer Science, pages 151–160. Sprin­ger-Verlag, 1991. Also INRIA Research Report.
[48]
G. Dowek. A Complete Proof Synthesis Method for the Cube of Type Systems. Journal Logic Computation, 3(3):287–315, June 1993.
[49]
G. Dowek. The undecidability of pattern matching in calculi where primitive recursive functions are representable. Theoretical Computer Science, 107(2):349–356, 1993.
[50]
G. Dowek. Third order matching is decidable. Annals of Pure and Applied Logic, 69:135–155, 1994.
[51]
G. Dowek. Lambda-calculus, combinators and the comprehension schema. In Proceedings of the second international conference on typed lambda calculus and applications, 1995.
[52]
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User’s Guide Version 5.8. Technical Report 154, INRIA, May 1993.
[53]
P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics: An inversion principle for Martin-Löf’s type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks, volume 14, pages 59–79. Cambridge University Press, 1991.
[54]
Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic, 57(3), September 1992.
[55]
J.-C. Filliâtre. Une procédure de décision pour le calcul des prédicats direct. Étude et implémentation dans le système Coq. Master’s thesis, DEA d’Informatique, ENS Lyon, September 1994.
[56]
J.-C. Filliâtre. A decision procedure for direct predicate calculus. Research report 96–25, LIP-ENS-Lyon, 1995.
[57]
J.-C. Filliâtre. Preuve de programmes impératifs en théorie des types. Thèse de doctorat, Université Paris-Sud, July 1999.
[58]
J.-C. Filliâtre. Formal Proof of a Program: Find. Submitted to Science of Computer Programming, January 2000.
[59]
J.-C. Filliâtre and N. Magaud. Certification of sorting algorithms in the system Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999.
[60]
J.-C. Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709–745, July 2003. [English translation of [57]].
[61]
E. Fleury. Implantation des algorithmes de Floyd et de Dijkstra dans le Calcul des Constructions. Rapport de Stage, July 1990.
[62]
Projet Formel. The Calculus of Constructions. Documentation and user’s guide, Version 4.10. Technical Report 110, INRIA, 1989.
[63]
Jean-Baptiste-Joseph Fourier. Fourier’s method to solve linear inequations/equations systems. Gauthier-Villars, 1890.
[64]
H. Geuvers and F. Wiedijk, editors. Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, volume 2646 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 2003.
[65]
E. Giménez. Codifying guarded definitions with recursive schemes. In Types’94 : Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 1994. Extended version in LIP research report 95-07, ENS Lyon.
[66]
E. Giménez. An application of co-inductive types in coq: verification of the alternating bit protocol. In Workshop on Types for Proofs and Programs, number 1158 in Lecture Notes in Computer Science, pages 135–152. Sprin­ger-Verlag, 1995.
[67]
E. Giménez. A tutorial on recursive types in coq. Technical report, INRIA, March 1998.
[68]
E. Giménez and P. Castéran. A tutorial on [co-]inductive types in coq. available at http://coq.inria.fr/doc, January 2005.
[69]
Alessandro Giovini, Teo Mora, Gianfranco Niesi, Lorenzo Robbiano, and Carlo Traverso. "one sugar cube, please" or selection strategies in the buchberger algorithm. In Proceedings of the ISSAC’91, ACM Press, pages 5–4, 1991.
[70]
J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In Proceedings of the 2nd Scandinavian Logic Symposium. North-Holland, 1970.
[71]
J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris 7, 1972.
[72]
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.
[73]
John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre,, 1995.
[74]
D. Hirschkoff. Écriture d’une tactique arithmétique pour le système Coq. Master’s thesis, DEA IARFA, Ecole des Ponts et Chaussées, Paris, September 1994.
[75]
Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Proceedings of the meeting Twenty-five years of constructive type theory. Oxford University Press, 1998.
[76]
W.A. Howard. The formulae-as-types notion of constructions. In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980. Unpublished 1969 Manuscript.
[77]
G. Huet. Programming of future generation computers. In Proceedings of TAPSOFT87, volume 249 of Lecture Notes in Computer Science, pages 276–286. Sprin­ger-Verlag, 1987.
[78]
G. Huet. Induction principles formalized in the Calculus of Constructions. In K. Fuchi and M. Nivat, editors, Programming of Future Generation Computers. Elsevier Science, 1988. Also in [77].
[79]
G. Huet, editor. Logical Foundations of Functional Programming. The UT Year of Programming Series. Addison-Wesley, 1989.
[80]
G. Huet. The Constructive Engine. In R. Narasimhan, editor, A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney. World Scientific Publishing, 1989. Also in [62].
[81]
G. Huet. The gallina specification language : A case study. In Proceedings of 12th FST/TCS Conference, New Delhi, volume 652 of Lecture Notes in Computer Science, pages 229–240. Sprin­ger-Verlag, 1992.
[82]
G. Huet. Residual theory in λ-calculus: a formal development. J. Functional Programming, 4,3:371–394, 1994.
[83]
G. Huet and J.-J. Lévy. Call by need computations in non-ambigous linear term rewriting systems. In J.-L. Lassez and G. Plotkin, editors, Computational Logic, Essays in Honor of Alan Robinson. The MIT press, 1991. Also research report 359, INRIA, 1979.
[84]
G. Huet and G. Plotkin, editors. Logical Frameworks. Cambridge University Press, 1991.
[85]
G. Huet and G. Plotkin, editors. Logical Environments. Cambridge University Press, 1992.
[86]
J. Ketonen and R. Weyhrauch. A decidable fragment of Predicate Calculus. Theoretical Computer Science, 32:297–307, 1984.
[87]
S.C. Kleene. Introduction to Metamathematics. Bibliotheca Mathematica. North-Holland, 1952.
[88]
J.-L. Krivine. Lambda-calcul types et modèles. Etudes et recherche en informatique. Masson, 1990.
[89]
A. Laville. Comparison of priority rules in pattern matching and term rewriting. Journal of Symbolic Computation, 11:321–347, 1991.
[90]
F. Leclerc and C. Paulin-Mohring. Programming with Streams in Coq. A case study : The Sieve of Eratosthenes. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, Types’ 93, volume 806 of LNCS. Sprin­ger-Verlag, 1994.
[91]
X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA, 1990.
[92]
P. Letouzey. A new extraction for coq. In Geuvers and Wiedijk [64].
[93]
L.Puel and A. Suárez. Compiling Pattern Matching by Term Decomposition. In Conference Lisp and Functional Programming, ACM. Sprin­ger-Verlag, 1990.
[94]
Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.
[95]
P. Manoury. A User’s Friendly Syntax to Define Recursive Functions as Typed λ−Terms. In Types for Proofs and Programs, TYPES’94, volume 996 of LNCS, June 1994.
[96]
P. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. TCS, 135(2):319–343, 1994.
[97]
L. Maranget. Two Techniques for Compiling Lazy Pattern Matching. Technical Report 2385, INRIA, 1994.
[98]
Conor McBride. Elimination with a motive. In Callaghan et al. [20], pages 197–216.
[99]
A. Miquel. A model for impredicative type systems with universes, intersection types and subtyping. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS’00). IEEE Computer Society Press, 2000.
[100]
A. Miquel. The implicit calculus of constructions: Extending pure type systems with an intersection type binder and subtyping. In Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland, number 2044 in LNCS. Sprin­ger-Verlag, 2001.
[101]
A. Miquel. Le Calcul des Constructions implicite: syntaxe et sémantique. PhD thesis, Université Paris 7, dec 2001.
[102]
A. Miquel and B. Werner. The not so simple proof-irrelevant model of cc. In Geuvers and Wiedijk [64], pages 240–258.
[103]
C. Muñoz. Un calcul de substitutions pour la représentation de preuves partielles en théorie de types. Thèse de doctorat, Université Paris 7, 1997. Version en anglais disponible comme rapport de recherche INRIA RR-3309.
[104]
C. Muñoz. Démonstration automatique dans la logique propositionnelle intuitionniste. Master’s thesis, DEA d’Informatique Fondamentale, Université Paris 7, September 1994.
[105]
B. Nordström. Terminating general recursion. BIT, 28, 1988.
[106]
B. Nordström, K. Peterson, and J. Smith. Programming in Martin-Löf’s Type Theory. International Series of Monographs on Computer Science. Oxford Science Publications, 1990.
[107]
B. Nordström, K. Petersson, and G. Plotkin, editors. Proceedings of the 1992 Workshop on Types for Proofs and Programs. Available by ftp at site ftp.inria.fr, 1992.
[108]
P. Odifreddi, editor. Logic and Computer Science. Academic Press, 1990.
[109]
P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984.
[110]
C. Parent. Developing certified programs in the system Coq- The Program tactic. Technical Report 93-29, Ecole Normale Supérieure de Lyon, October 1993. Also in [7].
[111]
C. Parent. Synthèse de preuves de programmes dans le Calcul des Constructions Inductives. PhD thesis, Ecole Normale Supérieure de Lyon, 1995.
[112]
C. Parent. Synthesizing proofs from programs in the Calculus of Inductive Constructions. In Mathematics of Program Construction’95, volume 947 of LNCS. Sprin­ger-Verlag, 1995.
[113]
M. Parigot. Recursive Programming with Proofs. Theoretical Computer Science, 94(2):335–356, 1992.
[114]
M. Parigot, P. Manoury, and M. Simonot. ProPre : A Programming language with proofs. In A. Voronkov, editor, Logic Programming and automated reasoning, number 624 in LNCS, St. Petersburg, Russia, July 1992. Sprin­ger-Verlag.
[115]
C. Paulin-Mohring. Extracting Fω’s programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM.
[116]
C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Université Paris 7, January 1989.
[117]
C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in LNCS. Sprin­ger-Verlag, 1993. Also LIP research report 92-49, ENS Lyon.
[118]
C. Paulin-Mohring. Le système Coq. Thèse d’habilitation. ENS Lyon, January 1997.
[119]
C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607–640, 1993.
[120]
K.V. Prasad. Programming with broadcasts. In Proceedings of CONCUR’93, volume 715 of LNCS. Sprin­ger-Verlag, 1993.
[121]
W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Communication of the ACM, pages 102–114, 1992.
[122]
J. Rouyer. Développement de l’Algorithme d’Unification dans le Calcul des Constructions. Technical Report 1795, INRIA, November 1992.
[123]
John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709–720, September 1998.
[124]
A. Saïbi. Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System. Technical Report 2345, INRIA, December 1994.
[125]
H. Saidi. Résolution d’équations dans le système t de gödel. Master’s thesis, DEA d’Informatique Fondamentale, Université Paris 7, September 1994.
[126]
Matthieu Sozeau. Subset coercions in Coq. In TYPES’06, volume 4502 of LNCS, pages 237–252. Springer, 2007.
[127]
Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In TPHOLs’08, 2008.
[128]
T. Streicher. Semantical investigations into intensional type theory, 1993. Habilitationsschrift, LMU Munchen.
[129]
Lemme Team. Pcoq a graphical user-interface for Coq. http://www-sop.inria.fr/lemme/pcoq/.
[130]
The Coq Development Team. The Coq Proof Assistant Reference Manual Version 7.2. Technical Report 255, INRIA, February 2002.
[131]
D. Terrasse. Traduction de TYPOL en COQ. Application à Mini ML. Master’s thesis, IARFA, September 1992.
[132]
L. Théry, Y. Bertot, and G. Kahn. Real theorem provers deserve real user-interfaces. Research Report 1684, INRIA Sophia, May 1992.
[133]
A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, an introduction. Studies in Logic and the foundations of Mathematics, volumes 121 and 123. North-Holland, 1988.
[134]
P. Wadler. Efficient compilation of pattern matching. In S.L. Peyton Jones, editor, The Implementation of Functional Programming Languages. Prentice-Hall, 1987.
[135]
P. Weis and X. Leroy. Le langage Caml. InterEditions, 1993.
[136]
B. Werner. Une théorie des constructions inductives. Thèse de doctorat, Université Paris 7, 1994.