2
@STRING{toappear="To appear"}
3
@STRING{lncs="Lecture Notes in Computer Science"}
6
AUTHOR = {Bruno~Barras, Samuel~Boutin,
7
Cristina~Cornes, Judica�l~Courant, Yann~Coscoy, David~Delahaye,
8
Daniel~de~Rauglaudre, Jean-Christophe~Filli�tre, Eduardo~Gim�nez,
9
Hugo~Herbelin, G�rard~Huet, Henri~Laulh�re, C�sar~Mu�oz,
10
Chetan~Murthy, Catherine~Parent-Vigouroux, Patrick~Loiseleur,
11
Christine~Paulin-Mohring, Amokrane~Sa�bi, Benjamin~Werner},
12
INSTITUTION = {INRIA},
13
TITLE = {{The Coq Proof Assistant Reference Manual -- Version V6.2}},
18
AUTHOR = {Ph. Audebaud},
19
BOOKTITLE = {Proceedings of the sixth Conf. on Logic in Computer Science.},
21
TITLE = {Partial {Objects} in the {Calculus of Constructions}},
26
AUTHOR = {Ph. Audebaud},
27
SCHOOL = {{Universit\'e} Bordeaux I},
28
TITLE = {Extension du Calcul des Constructions par Points fixes},
32
@INPROCEEDINGS{Audebaud92b,
33
AUTHOR = {Ph. Audebaud},
34
BOOKTITLE = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
35
EDITOR = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
36
NOTE = {Also Research Report LIP-ENS-Lyon},
38
TITLE = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
42
@INPROCEEDINGS{Augustsson85,
43
AUTHOR = {L. Augustsson},
44
TITLE = {{Compiling Pattern Matching}},
45
BOOKTITLE = {Conference Functional Programming and
46
Computer Architecture},
51
AUTHOR = {E. Gim\'enez},
52
EDITORS = {P. Dybjer and B. Nordstr\"om and J. Smith},
53
BOOKTITLE = {Workshop on Types for Proofs and Programs},
57
TITLE = {{Codifying guarded definitions with recursive schemes}},
59
PUBLISHER = {Springer-Verlag},
63
AUTHOR = {E. Gim\'enez},
64
BOOKTITLE = {Workshop on Types for Proofs and Programs},
68
TITLE = {An application of co-Inductive types in Coq:
69
verification of the Alternating Bit Protocol},
70
EDITORS = {S. Berardi and M. Coppo},
71
PUBLISHER = {Springer-Verlag},
76
author = {E. Gim\'enez},
77
title = {A Calculus of Infinite Constructions and its
78
application to the verification of communicating systems},
79
school = {Ecole Normale Sup\'erieure de Lyon},
84
AUTHOR = {J.L. Bates and R.L. Constable},
85
JOURNAL = {ACM transactions on Programming Languages and Systems},
86
TITLE = {Proofs as {Programs}},
92
AUTHOR = {H.P. Barendregt},
93
PUBLISHER = {North-Holland},
94
TITLE = {The Lambda Calculus its Syntax and Semantics},
99
AUTHOR = {H. Barendregt},
100
INSTITUTION = {Catholic University Nijmegen},
101
NOTE = {In Handbook of Logic in Computer Science, Vol II},
103
TITLE = {Lambda {Calculi with Types}},
108
EDITOR = {B. Nordstr\"om and K. Petersson and G. Plotkin},
109
PUBLISHER = {Available by ftp at site ftp.inria.fr},
110
TITLE = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
115
AUTHOR = {M.J. Beeson},
116
PUBLISHER = {Springer-Verlag},
117
TITLE = {Foundations of Constructive Mathematics, Metamathematical Studies},
122
AUTHOR = {G. Bellin and J. Ketonen},
123
JOURNAL = {Theoretical Computer Science},
125
TITLE = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
131
AUTHOR = {E. Bishop},
132
PUBLISHER = {McGraw-Hill},
133
TITLE = {Foundations of Constructive Analysis},
138
AUTHOR = {R.S. Boyer and J.S. Moore},
140
PUBLISHER = {Academic Press},
141
SERIES = {ACM Monograph},
142
TITLE = {A computational logic},
146
@MASTERSTHESIS{Bou92,
147
AUTHOR = {S. Boutin},
149
SCHOOL = {{Universit\'e Paris 7}},
150
TITLE = {Certification d'un compilateur {ML en Coq}},
155
AUTHOR = {N.J. de Bruijn},
156
JOURNAL = {Indag. Math.},
157
TITLE = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
163
AUTHOR = {N.J. de Bruijn},
164
BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
165
EDITOR = {J.P. Seldin and J.R. Hindley},
166
PUBLISHER = {Academic Press},
167
TITLE = {A survey of the project {Automath}},
173
TITLE = {The {ZINC} experiment: an economical implementation
174
of the {ML} language},
175
INSTITUTION = {INRIA},
181
AUTHOR = {P. Weis and X. Leroy},
182
PUBLISHER = {InterEditions},
183
TITLE = {Le langage Caml},
188
AUTHOR = {Projet Formel},
189
INSTITUTION = {INRIA},
191
TITLE = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
195
@INPROCEEDINGS{CoHu85a,
196
AUTHOR = {Th. Coquand and G. Huet},
198
BOOKTITLE = {EUROCAL'85},
199
PUBLISHER = {Springer-Verlag},
201
TITLE = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
207
author = {B. Barras},
208
title = {A formalisation of
209
\uppercase{B}urali-\uppercase{F}orti's paradox in Coq},
210
howpublished = {Distributed within the bunch of contribution to the
214
note = {\texttt{http://pauillac.inria.fr/coq}}
218
@INPROCEEDINGS{CoHu85b,
219
AUTHOR = {Th. Coquand and G. Huet},
220
BOOKTITLE = {Logic Colloquium'85},
221
EDITOR = {The Paris Logic Group},
222
PUBLISHER = {North-Holland},
223
TITLE = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}},
228
AUTHOR = {Th. Coquand and G. Huet},
229
JOURNAL = {Information and Computation},
231
TITLE = {The {Calculus of Constructions}},
237
AUTHOR = {R.L. {Constable et al.}},
238
PUBLISHER = {Prentice-Hall},
239
TITLE = {{Implementing Mathematics with the Nuprl Proof Development System}},
243
@INPROCEEDINGS{CoPa89,
244
AUTHOR = {Th. Coquand and C. Paulin-Mohring},
245
BOOKTITLE = {Proceedings of Colog'88},
246
EDITOR = {P. Martin-L{\"o}f and G. Mints},
247
PUBLISHER = {Springer-Verlag},
249
TITLE = {Inductively defined types},
255
AUTHOR = {Th. Coquand},
257
SCHOOL = {Universit\'e Paris~7},
258
TITLE = {Une Th\'eorie des Constructions},
262
@INPROCEEDINGS{Coq86,
263
AUTHOR = {Th. Coquand},
264
ADDRESS = {Cambridge, MA},
265
BOOKTITLE = {Symposium on Logic in Computer Science},
266
PUBLISHER = {IEEE Computer Society Press},
267
TITLE = {{An Analysis of Girard's Paradox}},
271
@INPROCEEDINGS{Coq90,
272
AUTHOR = {Th. Coquand},
273
BOOKTITLE = {Logic and Computer Science},
274
EDITOR = {P. Oddifredi},
275
NOTE = {INRIA Research Report 1088, also in~\cite{CoC89}},
276
PUBLISHER = {Academic Press},
277
TITLE = {{Metamathematical Investigations of a Calculus of Constructions}},
281
@INPROCEEDINGS{Coq92,
282
AUTHOR = {Th. Coquand},
283
BOOKTITLE = {in \cite{Bastad92}},
284
TITLE = {{Pattern Matching with Dependent Types}},
286
crossref = {Bastad92}
290
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},
291
INSTITUTION = {INRIA},
294
TITLE = {{The Coq Proof Assistant User's Guide Version 5.8}},
298
@INPROCEEDINGS{Coquand93,
299
AUTHOR = {Th. Coquand},
300
BOOKTITLE = {in \cite{Nijmegen93}},
301
TITLE = {{Infinite Objects in Type Theory}},
303
crossref = {Nijmegen93}
306
@MASTERSTHESIS{Cou94a,
307
AUTHOR = {J. Courant},
309
SCHOOL = {DEA d'Informatique, ENS Lyon},
310
TITLE = {Explicitation de preuves par r\'ecurrence implicite},
315
AUTHOR = {C. Parent},
316
INSTITUTION = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
318
NOTE = {Also in~\cite{Nijmegen93}},
320
TITLE = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
325
AUTHOR = {C. Parent},
326
SCHOOL = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
327
TITLE = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
333
INSTITUTION = {INRIA},
335
TITLE = {{Naming and Scoping in a Mathematical Vernacular}},
336
TYPE = {Research Report},
342
JOURNAL = {{Compte Rendu de l'Acad\'emie des Sciences}},
343
NOTE = {(The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors)},
346
TITLE = {{L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}},
351
@INPROCEEDINGS{Dow91b,
353
BOOKTITLE = {Proceedings of Mathematical Foundation of Computer Science},
354
NOTE = {Also INRIA Research Report},
356
PUBLISHER = {Springer-Verlag},
358
TITLE = {{A Second Order Pattern Matching Algorithm in the Cube of Typed {$\lambda$}-calculi}},
366
SCHOOL = {{Universit\'e Paris 7}},
367
TITLE = {{D\'emonstration automatique dans le Calcul des Constructions}},
373
TITLE = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
374
JOURNAL = {Journal Logic Computation},
384
NOTE = {To appear in Theoretical Computer Science},
385
TITLE = {{The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}},
391
JOURNAL = {Annals of Pure and Applied Logic},
394
TITLE = {Third order matching is decidable},
398
@INPROCEEDINGS{Dow94b,
400
BOOKTITLE = {Proceedings of the second international conference on typed lambda calculus and applications},
401
TITLE = {{Lambda-calculus, Combinators and the Comprehension Schema}},
405
@INPROCEEDINGS{Dyb91,
406
AUTHOR = {P. Dybjer},
407
BOOKTITLE = {Logical Frameworks},
408
EDITOR = {G. Huet and G. Plotkin},
410
PUBLISHER = {Cambridge University Press},
411
TITLE = {{Inductive sets and families in {Martin-L{\"o}f's Type Theory} and their set-theoretic semantics : An inversion principle for {Martin-L\"of's} type theory}},
417
AUTHOR = {Roy Dyckhoff},
418
JOURNAL = {The Journal of Symbolic Logic},
421
TITLE = {Contraction-free sequent calculi for intuitionistic logic},
426
@MASTERSTHESIS{Fil94,
427
AUTHOR = {J.-C. Filli\^atre},
429
SCHOOL = {DEA d'Informatique, ENS Lyon},
430
TITLE = {Une proc\'edure de d\'ecision pour le {C}alcul des {P}r\'edicats {D}irect. {E}tude et impl\'ementation dans le syst\`eme {C}oq},
434
@TECHREPORT{Filliatre95,
435
AUTHOR = {J.-C. Filli\^atre},
436
INSTITUTION = {LIP-ENS-Lyon},
437
TITLE = {{A decision procedure for Direct Predicate Calculus}},
438
TYPE = {Research report},
444
AUTHOR = {E. Fleury},
446
NOTE = {Rapport de Stage},
447
TITLE = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
453
author = {E. Gim\'nez},
454
title = {A Tutorial on Recursive Types in Coq},
455
institution = {INRIA},
460
author = {G. Huet and G. Kahn and Ch. Paulin-Mohring},
461
title = {The {Coq} Proof Assistant - A tutorial, Version 6.1},
462
institution = {INRIA},
463
type = {rapport technique},
466
note = {Version r�vis�e distribu�e avec {Coq}},
475
@INPROCEEDINGS{Gir70,
476
AUTHOR = {J.-Y. Girard},
477
BOOKTITLE = {Proceedings of the 2nd Scandinavian Logic Symposium},
478
PUBLISHER = {North-Holland},
479
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},
484
AUTHOR = {J.-Y. Girard},
485
SCHOOL = {Universit\'e Paris~7},
486
TITLE = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
491
AUTHOR = {J.-Y. Girard and Y. Lafont and P. Taylor},
492
PUBLISHER = {Cambridge University Press},
493
SERIES = {Cambridge Tracts in Theoretical Computer Science 7},
494
TITLE = {Proofs and Types},
498
@MASTERSTHESIS{Hir94,
499
AUTHOR = {D. Hirschkoff},
501
SCHOOL = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
502
TITLE = {{Ecriture d'une tactique arithm\'etique pour le syst\`eme Coq}},
507
AUTHOR = {W.A. Howard},
508
BOOKTITLE = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
509
EDITOR = {J.P. Seldin and J.R. Hindley},
510
NOTE = {Unpublished 1969 Manuscript},
511
PUBLISHER = {Academic Press},
512
TITLE = {The Formulae-as-Types Notion of Constructions},
516
@INCOLLECTION{HuetLevy79,
517
AUTHOR = {G. Huet and J.-J. L\'{e}vy},
518
TITLE = {Call by Need Computations in Non-Ambigous
519
Linear Term Rewriting Systems},
520
NOTE = {Also research report 359, INRIA, 1979},
521
BOOKTITLE = {Computational Logic, Essays in Honor of
523
EDITOR = {J.-L. Lassez and G. Plotkin},
524
PUBLISHER = {The MIT press},
528
@INPROCEEDINGS{Hue87,
530
BOOKTITLE = {Programming of Future Generation Computers},
531
EDITOR = {K. Fuchi and M. Nivat},
532
NOTE = {Also in Proceedings of TAPSOFT87, LNCS 249, Springer-Verlag, 1987, pp 276--286},
533
PUBLISHER = {Elsevier Science},
534
TITLE = {Induction Principles Formalized in the {Calculus of Constructions}},
538
@INPROCEEDINGS{Hue88,
540
BOOKTITLE = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
541
EDITOR = {R. Narasimhan},
542
NOTE = {Also in~\cite{CoC89}},
543
PUBLISHER = {World Scientific Publishing},
544
TITLE = {{The Constructive Engine}},
550
PUBLISHER = {Addison-Wesley},
551
SERIES = {The UT Year of Programming Series},
552
TITLE = {Logical Foundations of Functional Programming},
556
@INPROCEEDINGS{Hue92,
558
BOOKTITLE = {Proceedings of 12th FST/TCS Conference, New Delhi},
560
PUBLISHER = {Springer Verlag},
562
TITLE = {{The Gallina Specification Language : A case study}},
569
JOURNAL = {J. Functional Programming},
571
PUBLISHER = {Cambridge University Press},
572
TITLE = {Residual theory in $\lambda$-calculus: a formal development},
578
AUTHOR = {J. Ketonen and R. Weyhrauch},
579
JOURNAL = {Theoretical Computer Science},
581
TITLE = {A decidable fragment of {P}redicate {C}alculus},
587
AUTHOR = {S.C. Kleene},
588
PUBLISHER = {North-Holland},
589
SERIES = {Bibliotheca Mathematica},
590
TITLE = {Introduction to Metamathematics},
595
AUTHOR = {J.-L. Krivine},
596
PUBLISHER = {Masson},
597
SERIES = {Etudes et recherche en informatique},
598
TITLE = {Lambda-calcul {types et mod\`eles}},
603
AUTHOR = {A. Laville},
604
TITLE = {Comparison of Priority Rules in Pattern
605
Matching and Term Rewriting},
606
JOURNAL = {Journal of Symbolic Computation},
613
EDITOR = {G. Huet and G. Plotkin},
614
PUBLISHER = {Cambridge University Press},
615
TITLE = {Logical Environments},
619
@INPROCEEDINGS{LePa94,
620
AUTHOR = {F. Leclerc and C. Paulin-Mohring},
621
BOOKTITLE = {{Types for Proofs and Programs, Types' 93}},
622
EDITOR = {H. Barendregt and T. Nipkow},
623
PUBLISHER = {Springer-Verlag},
625
TITLE = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
631
EDITOR = {G. Huet and G. Plotkin},
632
PUBLISHER = {Cambridge University Press},
633
TITLE = {Logical Frameworks},
638
AUTHOR = {{P. Martin-L\"of}},
639
PUBLISHER = {Bibliopolis},
640
SERIES = {Studies in Proof Theory},
641
TITLE = {Intuitionistic Type Theory},
645
@INPROCEEDINGS{manoury94,
646
AUTHOR = {P. Manoury},
647
TITLE = {{A User's Friendly Syntax to Define
648
Recursive Functions as Typed $\lambda-$Terms}},
649
BOOKTITLE = {{Types for Proofs and Programs, TYPES'94}},
657
AUTHOR = {P. Manoury and M. Simonot},
659
TITLE = {Automatizing termination proof of recursively defined function},
663
@TECHREPORT{maranget94,
664
AUTHOR = {L. Maranget},
665
INSTITUTION = {INRIA},
667
TITLE = {{Two Techniques for Compiling Lazy Pattern Matching}},
671
@INPROCEEDINGS{Moh89a,
672
AUTHOR = {C. Paulin-Mohring},
674
BOOKTITLE = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
677
TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
682
AUTHOR = {C. Paulin-Mohring},
684
SCHOOL = {{Universit\'e Paris 7}},
685
TITLE = {Extraction de programmes dans le {Calcul des Constructions}},
689
@INPROCEEDINGS{Moh93,
690
AUTHOR = {C. Paulin-Mohring},
691
BOOKTITLE = {Proceedings of the conference Typed Lambda Calculi and Applications},
692
EDITOR = {M. Bezem and J.-F. Groote},
693
NOTE = {Also LIP research report 92-49, ENS Lyon},
695
PUBLISHER = {Springer-Verlag},
697
TITLE = {{Inductive Definitions in the System Coq - Rules and Properties}},
701
@MASTERSTHESIS{Mun94,
702
AUTHOR = {C. Mu\~noz},
704
SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
705
TITLE = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
710
EDITOR = {H. Barendregt and T. Nipkow},
711
PUBLISHER = {Springer-Verlag},
713
TITLE = {Types for Proofs and Programs},
719
AUTHOR = {B. {Nordstr\"om} and K. Peterson and J. Smith},
720
BOOKTITLE = {Information Processing 83},
721
PUBLISHER = {Oxford Science Publications},
722
SERIES = {International Series of Monographs on Computer Science},
723
TITLE = {Programming in {Martin-L\"of's} Type Theory},
728
AUTHOR = {B. {Nordstr\"om}},
730
TITLE = {Terminating General Recursion},
736
EDITOR = {P. Odifreddi},
737
PUBLISHER = {Academic Press},
738
TITLE = {Logic and Computer Science},
742
@INPROCEEDINGS{PaMS92,
743
AUTHOR = {M. Parigot and P. Manoury and M. Simonot},
744
ADDRESS = {St. Petersburg, Russia},
745
BOOKTITLE = {Logic Programming and automated reasoning},
746
EDITOR = {A. Voronkov},
749
PUBLISHER = {Springer-Verlag},
751
TITLE = {{ProPre : A Programming language with proofs}},
756
AUTHOR = {M. Parigot},
757
JOURNAL = {Theoretical Computer Science},
760
TITLE = {{Recursive Programming with Proofs}},
765
@INPROCEEDINGS{Parent95b,
766
AUTHOR = {C. Parent},
767
BOOKTITLE = {{Mathematics of Program Construction'95}},
768
PUBLISHER = {Springer-Verlag},
770
TITLE = {{Synthesizing proofs from programs in
771
the Calculus of Inductive Constructions}},
777
AUTHOR = {C. Paulin-Mohring and B. Werner},
778
JOURNAL = {Journal of Symbolic Computation},
780
TITLE = {{Synthesis of ML programs in the system Coq}},
785
@INPROCEEDINGS{Prasad93,
786
AUTHOR = {K.V. Prasad},
787
BOOKTITLE = {{Proceedings of CONCUR'93}},
788
PUBLISHER = {Springer-Verlag},
790
TITLE = {{Programming with broadcasts}},
795
@INPROCEEDINGS{puel-suarez90,
796
AUTHOR = {L.Puel and A. Su\'arez},
797
BOOKTITLE = {{Conference Lisp and Functional Programming}},
799
PUBLISHER = {Springer-Verlag},
800
TITLE = {{Compiling Pattern Matching by Term
806
AUTHOR = {J. Rouyer},
808
NOTE = {To appear as a technical report},
809
TITLE = {{D\'eveloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
814
AUTHOR = {A. Sa\"{\i}bi},
815
INSTITUTION = {INRIA},
818
TITLE = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
822
@MASTERSTHESIS{saidi94,
825
SCHOOL = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
826
TITLE = {R\'esolution d'\'equations dans le syst\`eme T
831
@MASTERSTHESIS{Ter92,
832
AUTHOR = {D. Terrasse},
835
TITLE = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
839
@TECHREPORT{ThBeKa92,
840
AUTHOR = {L. Th\'ery and Y. Bertot and G. Kahn},
841
INSTITUTION = {INRIA Sophia},
844
TITLE = {Real theorem provers deserve real user-interfaces},
845
TYPE = {Research Report},
850
AUTHOR = {A.S. Troelstra and D. van Dalen},
851
PUBLISHER = {North-Holland},
852
SERIES = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
853
TITLE = {Constructivism in Mathematics, an introduction},
857
@INCOLLECTION{wadler87,
858
AUTHOR = {P. Wadler},
859
TITLE = {Efficient Compilation of Pattern Matching},
860
BOOKTITLE = {The Implementation of Functional Programming
862
EDITOR = {S.L. Peyton Jones},
863
PUBLISHER = {Prentice-Hall},
868
AUTHOR = {B. Werner},
869
SCHOOL = {Universit\'e Paris 7},
870
TITLE = {Une th\'eorie des constructions inductives},
871
TYPE = {Th\`ese de Doctorat},
added
removed
doc/RecTutorial/manbiblio.bib
