diff options
Diffstat (limited to 'doc/refman/biblio.bib')
| -rw-r--r-- | doc/refman/biblio.bib | 1273 |
1 files changed, 0 insertions, 1273 deletions
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib deleted file mode 100644 index f93b66f9..00000000 --- a/doc/refman/biblio.bib +++ /dev/null @@ -1,1273 +0,0 @@ -@String{jfp = "Journal of Functional Programming"} -@String{lncs = "Lecture Notes in Computer Science"} -@String{lnai = "Lecture Notes in Artificial Intelligence"} -@String{SV = "{Springer-Verlag}"} - -@InProceedings{Aud91, - author = {Ph. Audebaud}, - booktitle = {Proceedings of the sixth Conf. on Logic in Computer Science.}, - publisher = {IEEE}, - title = {Partial {Objects} in the {Calculus of Constructions}}, - year = {1991} -} - -@PhDThesis{Aud92, - author = {Ph. Audebaud}, - school = {{Universit\'e} Bordeaux I}, - title = {Extension du Calcul des Constructions par Points fixes}, - year = {1992} -} - -@InProceedings{Audebaud92b, - author = {Ph. Audebaud}, - booktitle = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, - editor = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, - note = {Also Research Report LIP-ENS-Lyon}, - pages = {21--34}, - title = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, - year = {1992} -} - -@InProceedings{Augustsson85, - author = {L. Augustsson}, - title = {{Compiling Pattern Matching}}, - booktitle = {Conference Functional Programming and -Computer Architecture}, - year = {1985} -} - -@Article{BaCo85, - author = {J.L. Bates and R.L. Constable}, - journal = {ACM transactions on Programming Languages and Systems}, - title = {Proofs as {Programs}}, - volume = {7}, - year = {1985} -} - -@Book{Bar81, - author = {H.P. Barendregt}, - publisher = {North-Holland}, - title = {The Lambda Calculus its Syntax and Semantics}, - year = {1981} -} - -@TechReport{Bar91, - author = {H. Barendregt}, - institution = {Catholic University Nijmegen}, - note = {In Handbook of Logic in Computer Science, Vol II}, - number = {91-19}, - title = {Lambda {Calculi with Types}}, - year = {1991} -} - -@Article{BeKe92, - author = {G. Bellin and J. Ketonen}, - journal = {Theoretical Computer Science}, - pages = {115--142}, - title = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, - volume = {95}, - year = {1992} -} - -@Book{Bee85, - author = {M.J. Beeson}, - publisher = SV, - title = {Foundations of Constructive Mathematics, Metamathematical Studies}, - year = {1985} -} - -@Book{Bis67, - author = {E. Bishop}, - publisher = {McGraw-Hill}, - title = {Foundations of Constructive Analysis}, - year = {1967} -} - -@Book{BoMo79, - author = {R.S. Boyer and J.S. Moore}, - key = {BoMo79}, - publisher = {Academic Press}, - series = {ACM Monograph}, - title = {A computational logic}, - year = {1979} -} - -@MastersThesis{Bou92, - author = {S. Boutin}, - month = sep, - school = {{Universit\'e Paris 7}}, - title = {Certification d'un compilateur {ML en Coq}}, - year = {1992} -} - -@InProceedings{Bou97, - title = {Using reflection to build efficient and certified decision procedure -s}, - author = {S. Boutin}, - booktitle = {TACS'97}, - editor = {Martin Abadi and Takahashi Ito}, - publisher = SV, - series = lncs, - volume = 1281, - year = {1997} -} - -@PhDThesis{Bou97These, - author = {S. Boutin}, - title = {R\'eflexions sur les quotients}, - school = {Paris 7}, - year = 1997, - type = {th\`ese d'Universit\'e}, - month = apr -} - -@Article{Bru72, - author = {N.J. de Bruijn}, - journal = {Indag. Math.}, - title = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}}, - volume = {34}, - year = {1972} -} - - -@InCollection{Bru80, - author = {N.J. de Bruijn}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - publisher = {Academic Press}, - title = {A survey of the project {Automath}}, - year = {1980} -} - -@TechReport{COQ93, - author = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, - institution = {INRIA}, - month = may, - number = {154}, - title = {{The Coq Proof Assistant User's Guide Version 5.8}}, - year = {1993} -} - -@TechReport{COQ02, - author = {The Coq Development Team}, - institution = {INRIA}, - month = Feb, - number = {255}, - title = {{The Coq Proof Assistant Reference Manual Version 7.2}}, - year = {2002} -} - -@TechReport{CPar93, - author = {C. Parent}, - institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - month = oct, - note = {Also in~\cite{Nijmegen93}}, - number = {93-29}, - title = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, - year = {1993} -} - -@PhDThesis{CPar95, - author = {C. Parent}, - school = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - title = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, - year = {1995} -} - -@Book{Caml, - author = {P. Weis and X. Leroy}, - publisher = {InterEditions}, - title = {Le langage Caml}, - year = {1993} -} - -@InProceedings{ChiPotSimp03, - author = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, - title = {Mathematical Quotients and Quotient Types in Coq}, - booktitle = {TYPES}, - crossref = {DBLP:conf/types/2002}, - year = {2002} -} - -@TechReport{CoC89, - author = {Projet Formel}, - institution = {INRIA}, - number = {110}, - title = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, - year = {1989} -} - -@InProceedings{CoHu85a, - author = {Th. Coquand and G. Huet}, - address = {Linz}, - booktitle = {EUROCAL'85}, - publisher = SV, - series = LNCS, - title = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, - volume = {203}, - year = {1985} -} - -@InProceedings{CoHu85b, - author = {Th. Coquand and G. Huet}, - booktitle = {Logic Colloquium'85}, - editor = {The Paris Logic Group}, - publisher = {North-Holland}, - title = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, - year = {1987} -} - -@Article{CoHu86, - author = {Th. Coquand and G. Huet}, - journal = {Information and Computation}, - number = {2/3}, - title = {The {Calculus of Constructions}}, - volume = {76}, - year = {1988} -} - -@InProceedings{CoPa89, - author = {Th. Coquand and C. Paulin-Mohring}, - booktitle = {Proceedings of Colog'88}, - editor = {P. Martin-L\"of and G. Mints}, - publisher = SV, - series = LNCS, - title = {Inductively defined types}, - volume = {417}, - year = {1990} -} - -@Book{Con86, - author = {R.L. {Constable et al.}}, - publisher = {Prentice-Hall}, - title = {{Implementing Mathematics with the Nuprl Proof Development System}}, - year = {1986} -} - -@PhDThesis{Coq85, - author = {Th. Coquand}, - month = jan, - school = {Universit\'e Paris~7}, - title = {Une Th\'eorie des Constructions}, - year = {1985} -} - -@InProceedings{Coq86, - author = {Th. Coquand}, - address = {Cambridge, MA}, - booktitle = {Symposium on Logic in Computer Science}, - publisher = {IEEE Computer Society Press}, - title = {{An Analysis of Girard's Paradox}}, - year = {1986} -} - -@InProceedings{Coq90, - author = {Th. Coquand}, - booktitle = {Logic and Computer Science}, - editor = {P. Oddifredi}, - note = {INRIA Research Report 1088, also in~\cite{CoC89}}, - publisher = {Academic Press}, - title = {{Metamathematical Investigations of a Calculus of Constructions}}, - year = {1990} -} - -@InProceedings{Coq91, - author = {Th. Coquand}, - booktitle = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, - title = {{A New Paradox in Type Theory}}, - month = {August}, - year = {1991} -} - -@InProceedings{Coq92, - author = {Th. Coquand}, - title = {{Pattern Matching with Dependent Types}}, - year = {1992}, - crossref = {Bastad92} -} - -@InProceedings{Coquand93, - author = {Th. Coquand}, - title = {{Infinite Objects in Type Theory}}, - year = {1993}, - crossref = {Nijmegen93} -} - -@inproceedings{Corbineau08types, - author = {P. Corbineau}, - title = {A Declarative Language for the Coq Proof Assistant}, - editor = {M. Miculan and I. Scagnetto and F. Honsell}, - booktitle = {TYPES '07, Cividale del Friuli, Revised Selected Papers}, - publisher = {Springer}, - series = LNCS, - volume = {4941}, - year = {2007}, - pages = {69-84}, - ee = {http://dx.doi.org/10.1007/978-3-540-68103-8_5}, -} - -@PhDThesis{Cor97, - author = {C. Cornes}, - month = nov, - school = {{Universit\'e Paris 7}}, - title = {Conception d'un langage de haut niveau de représentation de preuves}, - type = {Th\`ese de Doctorat}, - year = {1997} -} - -@MastersThesis{Cou94a, - author = {J. Courant}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Explicitation de preuves par r\'ecurrence implicite}, - year = {1994} -} - -@InProceedings{Del99, - author = {Delahaye, D.}, - title = {Information Retrieval in a Coq Proof Library using - Type Isomorphisms}, - booktitle = {Proceedings of TYPES '99, L\"okeberg}, - publisher = SV, - series = lncs, - year = {1999}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf TYPES99-SIsos.ps.gz}" -} - -@InProceedings{Del00, - author = {Delahaye, D.}, - title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}}, - booktitle = {Proceedings of Logic for Programming and Automated Reasoning - (LPAR), Reunion Island}, - publisher = SV, - series = LNCS, - volume = {1955}, - pages = {85--95}, - month = {November}, - year = {2000}, - url = - "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf LPAR2000-ltac.ps.gz}" -} - -@InProceedings{DelMay01, - author = {Delahaye, D. and Mayero, M.}, - title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}}, - booktitle = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier}, - publisher = {INRIA}, - month = {Janvier}, - year = {2001}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf JFLA2000-Field.ps.gz}" -} - -@TechReport{Dow90, - author = {G. Dowek}, - institution = {INRIA}, - number = {1283}, - title = {Naming and Scoping in a Mathematical Vernacular}, - type = {Research Report}, - year = {1990} -} - -@Article{Dow91a, - author = {G. Dowek}, - journal = {Compte-Rendus de l'Acad\'emie des Sciences}, - note = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, - number = {12}, - pages = {951--956}, - title = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, - volume = {I, 312}, - year = {1991} -} - -@InProceedings{Dow91b, - author = {G. Dowek}, - booktitle = {Proceedings of Mathematical Foundation of Computer Science}, - note = {Also INRIA Research Report}, - pages = {151--160}, - publisher = SV, - series = LNCS, - title = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, - volume = {520}, - year = {1991} -} - -@PhDThesis{Dow91c, - author = {G. Dowek}, - month = dec, - school = {Universit\'e Paris 7}, - title = {D\'emonstration automatique dans le Calcul des Constructions}, - year = {1991} -} - -@Article{Dow92a, - author = {G. Dowek}, - title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, - year = 1993, - journal = tcs, - volume = 107, - number = 2, - pages = {349-356} -} - -@Article{Dow94a, - author = {G. Dowek}, - journal = {Annals of Pure and Applied Logic}, - volume = {69}, - pages = {135--155}, - title = {Third order matching is decidable}, - year = {1994} -} - -@InProceedings{Dow94b, - author = {G. Dowek}, - booktitle = {Proceedings of the second international conference on typed lambda calculus and applications}, - title = {Lambda-calculus, Combinators and the Comprehension Schema}, - year = {1995} -} - -@InProceedings{Dyb91, - author = {P. Dybjer}, - booktitle = {Logical Frameworks}, - editor = {G. Huet and G. Plotkin}, - pages = {59--79}, - publisher = {Cambridge University Press}, - title = {Inductive sets and families in {Martin-Löf's} - Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, - volume = {14}, - year = {1991} -} - -@Article{Dyc92, - author = {Roy Dyckhoff}, - journal = {The Journal of Symbolic Logic}, - month = sep, - number = {3}, - title = {Contraction-free sequent calculi for intuitionistic logic}, - volume = {57}, - year = {1992} -} - -@MastersThesis{Fil94, - author = {J.-C. Filli\^atre}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}}, - year = {1994} -} - -@TechReport{Filliatre95, - author = {J.-C. Filli\^atre}, - institution = {LIP-ENS-Lyon}, - title = {A decision procedure for Direct Predicate Calculus}, - type = {Research report}, - number = {96--25}, - year = {1995} -} - -@Article{Filliatre03jfp, - author = {J.-C. Filliâtre}, - title = {Verification of Non-Functional Programs - using Interpretations in Type Theory}, - journal = jfp, - volume = 13, - number = 4, - pages = {709--745}, - month = jul, - year = 2003, - note = {[English translation of \cite{Filliatre99}]}, - url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, - topics = {team, lri}, - type_publi = {irevcomlec} -} - -@PhDThesis{Filliatre99, - author = {J.-C. Filli\^atre}, - title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, - type = {Thèse de Doctorat}, - school = {Universit\'e Paris-Sud}, - year = 1999, - month = {July}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} -} - -@Unpublished{Filliatre99c, - author = {J.-C. Filli\^atre}, - title = {{Formal Proof of a Program: Find}}, - month = {January}, - year = 2000, - note = {Submitted to \emph{Science of Computer Programming}}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} -} - -@InProceedings{FilliatreMagaud99, - author = {J.-C. Filli\^atre and N. Magaud}, - title = {Certification of sorting algorithms in the system {\Coq}}, - booktitle = {Theorem Proving in Higher Order Logics: - Emerging Trends}, - year = 1999, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} -} - -@Unpublished{Fle90, - author = {E. Fleury}, - month = jul, - note = {Rapport de Stage}, - title = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, - year = {1990} -} - -@Book{Fourier, - author = {Jean-Baptiste-Joseph Fourier}, - publisher = {Gauthier-Villars}, - title = {Fourier's method to solve linear - inequations/equations systems.}, - year = {1890} -} - -@InProceedings{Gim94, - author = {E. Gim\'enez}, - booktitle = {Types'94 : Types for Proofs and Programs}, - note = {Extended version in LIP research report 95-07, ENS Lyon}, - publisher = SV, - series = LNCS, - title = {Codifying guarded definitions with recursive schemes}, - volume = {996}, - year = {1994} -} - -@TechReport{Gim98, - author = {E. Gim\'enez}, - title = {A Tutorial on Recursive Types in Coq}, - institution = {INRIA}, - year = 1998, - month = mar -} - -@Unpublished{GimCas05, - author = {E. Gim\'enez and P. Cast\'eran}, - title = {A Tutorial on [Co-]Inductive Types in Coq}, - institution = {INRIA}, - year = 2005, - month = jan, - note = {available at \url{http://coq.inria.fr/doc}} -} - -@InProceedings{Gimenez95b, - author = {E. Gim\'enez}, - booktitle = {Workshop on Types for Proofs and Programs}, - series = LNCS, - number = {1158}, - pages = {135-152}, - title = {An application of co-Inductive types in Coq: - verification of the Alternating Bit Protocol}, - editorS = {S. Berardi and M. Coppo}, - publisher = SV, - year = {1995} -} - -@InProceedings{Gir70, - author = {J.-Y. Girard}, - booktitle = {Proceedings of the 2nd Scandinavian Logic Symposium}, - publisher = {North-Holland}, - title = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, - year = {1970} -} - -@PhDThesis{Gir72, - author = {J.-Y. Girard}, - school = {Universit\'e Paris~7}, - title = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, - year = {1972} -} - -@Book{Gir89, - author = {J.-Y. Girard and Y. Lafont and P. Taylor}, - publisher = {Cambridge University Press}, - series = {Cambridge Tracts in Theoretical Computer Science 7}, - title = {Proofs and Types}, - year = {1989} -} - -@TechReport{Har95, - author = {John Harrison}, - title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, - institution = {SRI International Cambridge Computer Science Research Centre,}, - year = 1995, - type = {Technical Report}, - number = {CRC-053}, - abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} -} - -@MastersThesis{Hir94, - author = {D. Hirschkoff}, - month = sep, - school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, - title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, - year = {1994} -} - -@InProceedings{HofStr98, - author = {Martin Hofmann and Thomas Streicher}, - title = {The groupoid interpretation of type theory}, - booktitle = {Proceedings of the meeting Twenty-five years of constructive type theory}, - publisher = {Oxford University Press}, - year = {1998} -} - -@InCollection{How80, - author = {W.A. Howard}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - note = {Unpublished 1969 Manuscript}, - publisher = {Academic Press}, - title = {The Formulae-as-Types Notion of Constructions}, - year = {1980} -} - -@InProceedings{Hue87tapsoft, - author = {G. Huet}, - title = {Programming of Future Generation Computers}, - booktitle = {Proceedings of TAPSOFT87}, - series = LNCS, - volume = 249, - pages = {276--286}, - year = 1987, - publisher = SV -} - -@InProceedings{Hue87, - author = {G. Huet}, - booktitle = {Programming of Future Generation Computers}, - editor = {K. Fuchi and M. Nivat}, - note = {Also in \cite{Hue87tapsoft}}, - publisher = {Elsevier Science}, - title = {Induction Principles Formalized in the {Calculus of Constructions}}, - year = {1988} -} - -@InProceedings{Hue88, - author = {G. Huet}, - booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, - editor = {R. Narasimhan}, - note = {Also in~\cite{CoC89}}, - publisher = {World Scientific Publishing}, - title = {{The Constructive Engine}}, - year = {1989} -} - -@Book{Hue89, - editor = {G. Huet}, - publisher = {Addison-Wesley}, - series = {The UT Year of Programming Series}, - title = {Logical Foundations of Functional Programming}, - year = {1989} -} - -@InProceedings{Hue92, - author = {G. Huet}, - booktitle = {Proceedings of 12th FST/TCS Conference, New Delhi}, - pages = {229--240}, - publisher = SV, - series = LNCS, - title = {The Gallina Specification Language : A case study}, - volume = {652}, - year = {1992} -} - -@Article{Hue94, - author = {G. Huet}, - journal = {J. Functional Programming}, - pages = {371--394}, - publisher = {Cambridge University Press}, - title = {Residual theory in $\lambda$-calculus: a formal development}, - volume = {4,3}, - year = {1994} -} - -@InCollection{HuetLevy79, - author = {G. Huet and J.-J. L\'{e}vy}, - title = {Call by Need Computations in Non-Ambigous -Linear Term Rewriting Systems}, - note = {Also research report 359, INRIA, 1979}, - booktitle = {Computational Logic, Essays in Honor of -Alan Robinson}, - editor = {J.-L. Lassez and G. Plotkin}, - publisher = {The MIT press}, - year = {1991} -} - -@Article{KeWe84, - author = {J. Ketonen and R. Weyhrauch}, - journal = {Theoretical Computer Science}, - pages = {297--307}, - title = {A decidable fragment of {P}redicate {C}alculus}, - volume = {32}, - year = {1984} -} - -@Book{Kle52, - author = {S.C. Kleene}, - publisher = {North-Holland}, - series = {Bibliotheca Mathematica}, - title = {Introduction to Metamathematics}, - year = {1952} -} - -@Book{Kri90, - author = {J.-L. Krivine}, - publisher = {Masson}, - series = {Etudes et recherche en informatique}, - title = {Lambda-calcul {types et mod\`eles}}, - year = {1990} -} - -@Book{LE92, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Environments}, - year = {1992} -} - -@Book{LF91, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Frameworks}, - year = {1991} -} - -@Article{Laville91, - author = {A. Laville}, - title = {Comparison of Priority Rules in Pattern -Matching and Term Rewriting}, - journal = {Journal of Symbolic Computation}, - volume = {11}, - pages = {321--347}, - year = {1991} -} - -@InProceedings{LePa94, - author = {F. Leclerc and C. Paulin-Mohring}, - booktitle = {{Types for Proofs and Programs, Types' 93}}, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = {LNCS}, - title = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, - volume = {806}, - year = {1994} -} - -@TechReport{Leroy90, - author = {X. Leroy}, - title = {The {ZINC} experiment: an economical implementation -of the {ML} language}, - institution = {INRIA}, - number = {117}, - year = {1990} -} - -@InProceedings{Let02, - author = {P. Letouzey}, - title = {A New Extraction for Coq}, - booktitle = {TYPES}, - year = 2002, - crossref = {DBLP:conf/types/2002}, - url = {draft at \url{http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz}} -} - -@PhDThesis{Luo90, - author = {Z. Luo}, - title = {An Extended Calculus of Constructions}, - school = {University of Edinburgh}, - year = {1990} -} - -@Book{MaL84, - author = {{P. Martin-L\"of}}, - publisher = {Bibliopolis}, - series = {Studies in Proof Theory}, - title = {Intuitionistic Type Theory}, - year = {1984} -} - -@Article{MaSi94, - author = {P. Manoury and M. Simonot}, - title = {Automatizing Termination Proofs of Recursively Defined Functions.}, - journal = {TCS}, - volume = {135}, - number = {2}, - year = {1994}, - pages = {319-343}, -} - -@InProceedings{Miquel00, - author = {A. Miquel}, - title = {A Model for Impredicative Type Systems with Universes, -Intersection Types and Subtyping}, - booktitle = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}}, - publisher = {IEEE Computer Society Press}, - year = {2000} -} - -@PhDThesis{Miquel01a, - author = {A. Miquel}, - title = {Le Calcul des Constructions implicite: syntaxe et s\'emantique}, - month = {dec}, - school = {{Universit\'e Paris 7}}, - year = {2001} -} - -@InProceedings{Miquel01b, - author = {A. Miquel}, - title = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping}, - booktitle = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}}, - publisher = SV, - series = {LNCS}, - number = 2044, - year = {2001} -} - -@InProceedings{MiWer02, - author = {A. Miquel and B. Werner}, - title = {The Not So Simple Proof-Irrelevant Model of CC}, - booktitle = {TYPES}, - year = {2002}, - pages = {240-258}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm}, - crossref = {DBLP:conf/types/2002}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2002, - editor = {H. Geuvers and F. Wiedijk}, - title = {Types for Proofs and Programs, Second International Workshop, - TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, - Selected Papers}, - booktitle = {TYPES}, - publisher = SV, - series = LNCS, - volume = {2646}, - year = {2003}, - isbn = {3-540-14031-X}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@InProceedings{Moh89a, - author = {C. Paulin-Mohring}, - address = {Austin}, - booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, - month = jan, - publisher = {ACM}, - title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, - year = {1989} -} - -@PhDThesis{Moh89b, - author = {C. Paulin-Mohring}, - month = jan, - school = {{Universit\'e Paris 7}}, - title = {Extraction de programmes dans le {Calcul des Constructions}}, - year = {1989} -} - -@InProceedings{Moh93, - author = {C. Paulin-Mohring}, - booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications}, - editor = {M. Bezem and J.-F. Groote}, - note = {Also LIP research report 92-49, ENS Lyon}, - number = {664}, - publisher = SV, - series = {LNCS}, - title = {{Inductive Definitions in the System Coq - Rules and Properties}}, - year = {1993} -} - -@Book{Moh97, - author = {C. Paulin-Mohring}, - month = jan, - publisher = {{ENS Lyon}}, - title = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, - year = {1997} -} - -@MastersThesis{Mun94, - author = {C. Muñoz}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, - year = {1994} -} - -@PhDThesis{Mun97d, - author = {C. Mu{\~{n}}oz}, - title = {Un calcul de substitutions pour la repr\'esentation - de preuves partielles en th\'eorie de types}, - school = {Universit\'e Paris 7}, - year = {1997}, - note = {Version en anglais disponible comme rapport de - recherche INRIA RR-3309}, - type = {Th\`ese de Doctorat} -} - -@Book{NoPS90, - author = {B. {Nordstr\"om} and K. Peterson and J. Smith}, - booktitle = {Information Processing 83}, - publisher = {Oxford Science Publications}, - series = {International Series of Monographs on Computer Science}, - title = {Programming in {Martin-L\"of's} Type Theory}, - year = {1990} -} - -@Article{Nor88, - author = {B. {Nordstr\"om}}, - journal = {BIT}, - title = {Terminating General Recursion}, - volume = {28}, - year = {1988} -} - -@Book{Odi90, - editor = {P. Odifreddi}, - publisher = {Academic Press}, - title = {Logic and Computer Science}, - year = {1990} -} - -@InProceedings{PaMS92, - author = {M. Parigot and P. Manoury and M. Simonot}, - address = {St. Petersburg, Russia}, - booktitle = {Logic Programming and automated reasoning}, - editor = {A. Voronkov}, - month = jul, - number = {624}, - publisher = SV, - series = {LNCS}, - title = {{ProPre : A Programming language with proofs}}, - year = {1992} -} - -@Article{PaWe92, - author = {C. Paulin-Mohring and B. Werner}, - journal = {Journal of Symbolic Computation}, - pages = {607--640}, - title = {{Synthesis of ML programs in the system Coq}}, - volume = {15}, - year = {1993} -} - -@Article{Par92, - author = {M. Parigot}, - journal = {Theoretical Computer Science}, - number = {2}, - pages = {335--356}, - title = {{Recursive Programming with Proofs}}, - volume = {94}, - year = {1992} -} - -@InProceedings{Parent95b, - author = {C. Parent}, - booktitle = {{Mathematics of Program Construction'95}}, - publisher = SV, - series = {LNCS}, - title = {{Synthesizing proofs from programs in -the Calculus of Inductive Constructions}}, - volume = {947}, - year = {1995} -} - -@InProceedings{Prasad93, - author = {K.V. Prasad}, - booktitle = {{Proceedings of CONCUR'93}}, - publisher = SV, - series = {LNCS}, - title = {{Programming with broadcasts}}, - volume = {715}, - year = {1993} -} - -@Book{RC95, - author = {di~Cosmo, R.}, - title = {Isomorphisms of Types: from $\lambda$-calculus to information - retrieval and language design}, - series = {Progress in Theoretical Computer Science}, - publisher = {Birkhauser}, - year = {1995}, - note = {ISBN-0-8176-3763-X} -} - -@TechReport{Rou92, - author = {J. Rouyer}, - institution = {INRIA}, - month = nov, - number = {1795}, - title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}}, - year = {1992} -} - -@Article{Rushby98, - title = {Subtypes for Specifications: Predicate Subtyping in - {PVS}}, - author = {John Rushby and Sam Owre and N. Shankar}, - journal = {IEEE Transactions on Software Engineering}, - pages = {709--720}, - volume = 24, - number = 9, - month = sep, - year = 1998 -} - -@TechReport{Saibi94, - author = {A. Sa\"{\i}bi}, - institution = {INRIA}, - month = dec, - number = {2345}, - title = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, - year = {1994} -} - - -@MastersThesis{Ter92, - author = {D. Terrasse}, - month = sep, - school = {IARFA}, - title = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, - year = {1992} -} - -@TechReport{ThBeKa92, - author = {L. Th\'ery and Y. Bertot and G. Kahn}, - institution = {INRIA Sophia}, - month = may, - number = {1684}, - title = {Real theorem provers deserve real user-interfaces}, - type = {Research Report}, - year = {1992} -} - -@Book{TrDa89, - author = {A.S. Troelstra and D. van Dalen}, - publisher = {North-Holland}, - series = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, - title = {Constructivism in Mathematics, an introduction}, - year = {1988} -} - -@PhDThesis{Wer94, - author = {B. Werner}, - school = {Universit\'e Paris 7}, - title = {Une th\'eorie des constructions inductives}, - type = {Th\`ese de Doctorat}, - year = {1994} -} - -@PhDThesis{Bar99, - author = {B. Barras}, - school = {Universit\'e Paris 7}, - title = {Auto-validation d'un système de preuves avec familles inductives}, - type = {Th\`ese de Doctorat}, - year = {1999} -} - -@Unpublished{ddr98, - author = {D. de Rauglaudre}, - title = {Camlp4 version 1.07.2}, - year = {1998}, - note = {In Camlp4 distribution} -} - -@Article{dowek93, - author = {G. Dowek}, - title = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, - journal = {Journal Logic Computation}, - volume = {3}, - number = {3}, - pages = {287--315}, - month = {June}, - year = {1993} -} - -@InProceedings{manoury94, - author = {P. Manoury}, - title = {{A User's Friendly Syntax to Define -Recursive Functions as Typed $\lambda-$Terms}}, - booktitle = {{Types for Proofs and Programs, TYPES'94}}, - series = {LNCS}, - volume = {996}, - month = jun, - year = {1994} -} - -@TechReport{maranget94, - author = {L. Maranget}, - institution = {INRIA}, - number = {2385}, - title = {{Two Techniques for Compiling Lazy Pattern Matching}}, - year = {1994} -} - -@InProceedings{puel-suarez90, - author = {L.Puel and A. Su\'arez}, - booktitle = {{Conference Lisp and Functional Programming}}, - series = {ACM}, - publisher = SV, - title = {{Compiling Pattern Matching by Term -Decomposition}}, - year = {1990} -} - -@MastersThesis{saidi94, - author = {H. Saidi}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {R\'esolution d'\'equations dans le syst\`eme T - de G\"odel}, - year = {1994} -} - -@inproceedings{sozeau06, - author = {Matthieu Sozeau}, - title = {Subset Coercions in {C}oq}, - year = {2007}, - booktitle = {TYPES'06}, - pages = {237-252}, - volume = {4502}, - publisher = "Springer", - series = {LNCS} -} - -@inproceedings{sozeau08, - Author = {Matthieu Sozeau and Nicolas Oury}, - booktitle = {TPHOLs'08}, - Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf}, - Title = {{F}irst-{C}lass {T}ype {C}lasses}, - Year = {2008}, -} - -@Misc{streicher93semantical, - author = {T. Streicher}, - title = {Semantical Investigations into Intensional Type Theory}, - note = {Habilitationsschrift, LMU Munchen.}, - year = {1993} -} - -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{http://proofgeneral.inf.ed.ac.uk/}} -} - -@Book{CoqArt, - title = {Interactive Theorem Proving and Program Development. - Coq'Art: The Calculus of Inductive Constructions}, - author = {Yves Bertot and Pierre Castéran}, - publisher = {Springer Verlag}, - series = {Texts in Theoretical Computer Science. An EATCS series}, - year = 2004 -} - -@InCollection{wadler87, - author = {P. Wadler}, - title = {Efficient Compilation of Pattern Matching}, - booktitle = {The Implementation of Functional Programming -Languages}, - editor = {S.L. Peyton Jones}, - publisher = {Prentice-Hall}, - year = {1987} -} - -@inproceedings{DBLP:conf/types/CornesT95, - author = {Cristina Cornes and - Delphine Terrasse}, - title = {Automating Inversion of Inductive Predicates in Coq}, - booktitle = {TYPES}, - year = {1995}, - pages = {85-104}, - crossref = {DBLP:conf/types/1995}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} -@proceedings{DBLP:conf/types/1995, - editor = {Stefano Berardi and - Mario Coppo}, - title = {Types for Proofs and Programs, International Workshop TYPES'95, - Torino, Italy, June 5-8, 1995, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {1158}, - year = {1996}, - isbn = {3-540-61780-9}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@inproceedings{DBLP:conf/types/McBride00, - author = {Conor McBride}, - title = {Elimination with a Motive}, - booktitle = {TYPES}, - year = {2000}, - pages = {197-216}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, - crossref = {DBLP:conf/types/2000}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2000, - editor = {Paul Callaghan and - Zhaohui Luo and - James McKinna and - Robert Pollack}, - title = {Types for Proofs and Programs, International Workshop, TYPES - 2000, Durham, UK, December 8-12, 2000, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {2277}, - year = {2002}, - isbn = {3-540-43287-6}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@INPROCEEDINGS{sugar, - author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso}, - title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm}, - booktitle = { Proceedings of the ISSAC'91, ACM Press}, - year = {1991}, - pages = {5--4}, - publisher = {} -} - -@Comment{cross-references, must be at end} - -@Book{Bastad92, - editor = {B. Nordstr\"om and K. Petersson and G. Plotkin}, - publisher = {Available by ftp at site ftp.inria.fr}, - title = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, - year = {1992} -} - -@Book{Nijmegen93, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = LNCS, - title = {Types for Proofs and Programs}, - volume = {806}, - year = {1994} -} - -@article{ TheOmegaPaper, - author = "W. Pugh", - title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis", - journal = "Communication of the ACM", - pages = "102--114", - year = "1992", -} |