1
@String{jfp = "Journal of Functional Programming"}
2
@String{lncs = "Lecture Notes in Computer Science"}
3
@String{lnai = "Lecture Notes in Artificial Intelligence"}
4
@String{SV = "{Sprin�ger-Verlag}"}
7
author = {Ph. Audebaud},
8
booktitle = {Proceedings of the sixth Conf. on Logic in Computer Science.},
10
title = {Partial {Objects} in the {Calculus of Constructions}},
15
author = {Ph. Audebaud},
16
school = {{Universit\'e} Bordeaux I},
17
title = {Extension du Calcul des Constructions par Points fixes},
21
@InProceedings{Audebaud92b,
22
author = {Ph. Audebaud},
23
booktitle = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
24
editor = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
25
note = {Also Research Report LIP-ENS-Lyon},
27
title = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
31
@InProceedings{Augustsson85,
32
author = {L. Augustsson},
33
title = {{Compiling Pattern Matching}},
34
booktitle = {Conference Functional Programming and
35
Computer Architecture},
40
author = {J.L. Bates and R.L. Constable},
41
journal = {ACM transactions on Programming Languages and Systems},
42
title = {Proofs as {Programs}},
48
author = {H.P. Barendregt},
49
publisher = {North-Holland},
50
title = {The Lambda Calculus its Syntax and Semantics},
55
author = {H. Barendregt},
56
institution = {Catholic University Nijmegen},
57
note = {In Handbook of Logic in Computer Science, Vol II},
59
title = {Lambda {Calculi with Types}},
64
author = {G. Bellin and J. Ketonen},
65
journal = {Theoretical Computer Science},
67
title = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
73
author = {M.J. Beeson},
75
title = {Foundations of Constructive Mathematics, Metamathematical Studies},
81
publisher = {McGraw-Hill},
82
title = {Foundations of Constructive Analysis},
87
author = {R.S. Boyer and J.S. Moore},
89
publisher = {Academic Press},
90
series = {ACM Monograph},
91
title = {A computational logic},
98
school = {{Universit\'e Paris 7}},
99
title = {Certification d'un compilateur {ML en Coq}},
103
@InProceedings{Bou97,
104
title = {Using reflection to build efficient and certified decision procedure
106
author = {S. Boutin},
107
booktitle = {TACS'97},
108
editor = {Martin Abadi and Takahashi Ito},
115
@PhDThesis{Bou97These,
116
author = {S. Boutin},
117
title = {R\'eflexions sur les quotients},
120
type = {th\`ese d'Universit\'e},
125
author = {N.J. de Bruijn},
126
journal = {Indag. Math.},
127
title = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
134
author = {N.J. de Bruijn},
135
booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
136
editor = {J.P. Seldin and J.R. Hindley},
137
publisher = {Academic Press},
138
title = {A survey of the project {Automath}},
143
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},
144
institution = {INRIA},
147
title = {{The Coq Proof Assistant User's Guide Version 5.8}},
152
author = {The Coq Development Team},
153
institution = {INRIA},
156
title = {{The Coq Proof Assistant Reference Manual Version 7.2}},
161
author = {C. Parent},
162
institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
164
note = {Also in~\cite{Nijmegen93}},
166
title = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
171
author = {C. Parent},
172
school = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
173
title = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
178
author = {P. Weis and X. Leroy},
179
publisher = {InterEditions},
180
title = {Le langage Caml},
184
@InProceedings{ChiPotSimp03,
185
author = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
186
title = {Mathematical Quotients and Quotient Types in Coq},
188
crossref = {DBLP:conf/types/2002},
193
author = {Projet Formel},
194
institution = {INRIA},
196
title = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
200
@InProceedings{CoHu85a,
201
author = {Th. Coquand and G. Huet},
203
booktitle = {EUROCAL'85},
206
title = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
211
@InProceedings{CoHu85b,
212
author = {Th. Coquand and G. Huet},
213
booktitle = {Logic Colloquium'85},
214
editor = {The Paris Logic Group},
215
publisher = {North-Holland},
216
title = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}},
221
author = {Th. Coquand and G. Huet},
222
journal = {Information and Computation},
224
title = {The {Calculus of Constructions}},
229
@InProceedings{CoPa89,
230
author = {Th. Coquand and C. Paulin-Mohring},
231
booktitle = {Proceedings of Colog'88},
232
editor = {P. Martin-L\"of and G. Mints},
235
title = {Inductively defined types},
241
author = {R.L. {Constable et al.}},
242
publisher = {Prentice-Hall},
243
title = {{Implementing Mathematics with the Nuprl Proof Development System}},
248
author = {Th. Coquand},
250
school = {Universit\'e Paris~7},
251
title = {Une Th\'eorie des Constructions},
255
@InProceedings{Coq86,
256
author = {Th. Coquand},
257
address = {Cambridge, MA},
258
booktitle = {Symposium on Logic in Computer Science},
259
publisher = {IEEE Computer Society Press},
260
title = {{An Analysis of Girard's Paradox}},
264
@InProceedings{Coq90,
265
author = {Th. Coquand},
266
booktitle = {Logic and Computer Science},
267
editor = {P. Oddifredi},
268
note = {INRIA Research Report 1088, also in~\cite{CoC89}},
269
publisher = {Academic Press},
270
title = {{Metamathematical Investigations of a Calculus of Constructions}},
274
@InProceedings{Coq91,
275
author = {Th. Coquand},
276
booktitle = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science},
277
title = {{A New Paradox in Type Theory}},
282
@InProceedings{Coq92,
283
author = {Th. Coquand},
284
title = {{Pattern Matching with Dependent Types}},
286
crossref = {Bastad92}
289
@InProceedings{Coquand93,
290
author = {Th. Coquand},
291
title = {{Infinite Objects in Type Theory}},
293
crossref = {Nijmegen93}
296
@inproceedings{Corbineau08types,
297
author = {P. Corbineau},
298
title = {A Declarative Language for the Coq Proof Assistant},
299
editor = {M. Miculan and I. Scagnetto and F. Honsell},
300
booktitle = {TYPES '07, Cividale del Friuli, Revised Selected Papers},
301
publisher = {Springer},
306
ee = {http://dx.doi.org/10.1007/978-3-540-68103-8_5},
310
author = {C. Cornes},
312
school = {{Universit\'e Paris 7}},
313
title = {Conception d'un langage de haut niveau de repr�sentation de preuves},
314
type = {Th\`ese de Doctorat},
318
@MastersThesis{Cou94a,
319
author = {J. Courant},
321
school = {DEA d'Informatique, ENS Lyon},
322
title = {Explicitation de preuves par r\'ecurrence implicite},
326
@InProceedings{Del99,
327
author = {Delahaye, D.},
328
title = {Information Retrieval in a Coq Proof Library using
330
booktitle = {Proceedings of TYPES '99, L\"okeberg},
335
"\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
336
"{\sf TYPES99-SIsos.ps.gz}"
339
@InProceedings{Del00,
340
author = {Delahaye, D.},
341
title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}},
342
booktitle = {Proceedings of Logic for Programming and Automated Reasoning
343
(LPAR), Reunion Island},
351
"{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
352
"{\sf LPAR2000-ltac.ps.gz}"
355
@InProceedings{DelMay01,
356
author = {Delahaye, D. and Mayero, M.},
357
title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}},
358
booktitle = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier},
363
"\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
364
"{\sf JFLA2000-Field.ps.gz}"
369
institution = {INRIA},
371
title = {Naming and Scoping in a Mathematical Vernacular},
372
type = {Research Report},
378
journal = {Compte-Rendus de l'Acad\'emie des Sciences},
379
note = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors},
382
title = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types},
387
@InProceedings{Dow91b,
389
booktitle = {Proceedings of Mathematical Foundation of Computer Science},
390
note = {Also INRIA Research Report},
394
title = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi},
402
school = {Universit\'e Paris 7},
403
title = {D\'emonstration automatique dans le Calcul des Constructions},
409
title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
419
journal = {Annals of Pure and Applied Logic},
422
title = {Third order matching is decidable},
426
@InProceedings{Dow94b,
428
booktitle = {Proceedings of the second international conference on typed lambda calculus and applications},
429
title = {Lambda-calculus, Combinators and the Comprehension Schema},
433
@InProceedings{Dyb91,
434
author = {P. Dybjer},
435
booktitle = {Logical Frameworks},
436
editor = {G. Huet and G. Plotkin},
438
publisher = {Cambridge University Press},
439
title = {Inductive sets and families in {Martin-L�f's}
440
Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory},
446
author = {Roy Dyckhoff},
447
journal = {The Journal of Symbolic Logic},
450
title = {Contraction-free sequent calculi for intuitionistic logic},
455
@MastersThesis{Fil94,
456
author = {J.-C. Filli\^atre},
458
school = {DEA d'Informatique, ENS Lyon},
459
title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. �tude et impl\'ementation dans le syst\`eme {\Coq}},
463
@TechReport{Filliatre95,
464
author = {J.-C. Filli\^atre},
465
institution = {LIP-ENS-Lyon},
466
title = {A decision procedure for Direct Predicate Calculus},
467
type = {Research report},
472
@Article{Filliatre03jfp,
473
author = {J.-C. Filli�tre},
474
title = {Verification of Non-Functional Programs
475
using Interpretations in Type Theory},
482
note = {[English translation of \cite{Filliatre99}]},
483
url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
484
topics = {team, lri},
485
type_publi = {irevcomlec}
488
@PhDThesis{Filliatre99,
489
author = {J.-C. Filli\^atre},
490
title = {Preuve de programmes imp\'eratifs en th\'eorie des types},
491
type = {Th�se de Doctorat},
492
school = {Universit\'e Paris-Sud},
495
url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}}
498
@Unpublished{Filliatre99c,
499
author = {J.-C. Filli\^atre},
500
title = {{Formal Proof of a Program: Find}},
503
note = {Submitted to \emph{Science of Computer Programming}},
504
url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}}
507
@InProceedings{FilliatreMagaud99,
508
author = {J.-C. Filli\^atre and N. Magaud},
509
title = {Certification of sorting algorithms in the system {\Coq}},
510
booktitle = {Theorem Proving in Higher Order Logics:
513
url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}}
517
author = {E. Fleury},
519
note = {Rapport de Stage},
520
title = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
525
author = {Jean-Baptiste-Joseph Fourier},
526
publisher = {Gauthier-Villars},
527
title = {Fourier's method to solve linear
528
inequations/equations systems.},
532
@InProceedings{Gim94,
533
author = {E. Gim\'enez},
534
booktitle = {Types'94 : Types for Proofs and Programs},
535
note = {Extended version in LIP research report 95-07, ENS Lyon},
538
title = {Codifying guarded definitions with recursive schemes},
544
author = {E. Gim\'enez},
545
title = {A Tutorial on Recursive Types in Coq},
546
institution = {INRIA},
551
@Unpublished{GimCas05,
552
author = {E. Gim\'enez and P. Cast\'eran},
553
title = {A Tutorial on [Co-]Inductive Types in Coq},
554
institution = {INRIA},
557
note = {available at \url{http://coq.inria.fr/doc}}
560
@InProceedings{Gimenez95b,
561
author = {E. Gim\'enez},
562
booktitle = {Workshop on Types for Proofs and Programs},
566
title = {An application of co-Inductive types in Coq:
567
verification of the Alternating Bit Protocol},
568
editorS = {S. Berardi and M. Coppo},
573
@InProceedings{Gir70,
574
author = {J.-Y. Girard},
575
booktitle = {Proceedings of the 2nd Scandinavian Logic Symposium},
576
publisher = {North-Holland},
577
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},
582
author = {J.-Y. Girard},
583
school = {Universit\'e Paris~7},
584
title = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
589
author = {J.-Y. Girard and Y. Lafont and P. Taylor},
590
publisher = {Cambridge University Press},
591
series = {Cambridge Tracts in Theoretical Computer Science 7},
592
title = {Proofs and Types},
597
author = {John Harrison},
598
title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique},
599
institution = {SRI International Cambridge Computer Science Research Centre,},
601
type = {Technical Report},
603
abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html}
606
@MastersThesis{Hir94,
607
author = {D. Hirschkoff},
609
school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
610
title = {�criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
614
@InProceedings{HofStr98,
615
author = {Martin Hofmann and Thomas Streicher},
616
title = {The groupoid interpretation of type theory},
617
booktitle = {Proceedings of the meeting Twenty-five years of constructive type theory},
618
publisher = {Oxford University Press},
623
author = {W.A. Howard},
624
booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
625
editor = {J.P. Seldin and J.R. Hindley},
626
note = {Unpublished 1969 Manuscript},
627
publisher = {Academic Press},
628
title = {The Formulae-as-Types Notion of Constructions},
632
@InProceedings{Hue87tapsoft,
634
title = {Programming of Future Generation Computers},
635
booktitle = {Proceedings of TAPSOFT87},
643
@InProceedings{Hue87,
645
booktitle = {Programming of Future Generation Computers},
646
editor = {K. Fuchi and M. Nivat},
647
note = {Also in \cite{Hue87tapsoft}},
648
publisher = {Elsevier Science},
649
title = {Induction Principles Formalized in the {Calculus of Constructions}},
653
@InProceedings{Hue88,
655
booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
656
editor = {R. Narasimhan},
657
note = {Also in~\cite{CoC89}},
658
publisher = {World Scientific Publishing},
659
title = {{The Constructive Engine}},
665
publisher = {Addison-Wesley},
666
series = {The UT Year of Programming Series},
667
title = {Logical Foundations of Functional Programming},
671
@InProceedings{Hue92,
673
booktitle = {Proceedings of 12th FST/TCS Conference, New Delhi},
677
title = {The Gallina Specification Language : A case study},
684
journal = {J. Functional Programming},
686
publisher = {Cambridge University Press},
687
title = {Residual theory in $\lambda$-calculus: a formal development},
692
@InCollection{HuetLevy79,
693
author = {G. Huet and J.-J. L\'{e}vy},
694
title = {Call by Need Computations in Non-Ambigous
695
Linear Term Rewriting Systems},
696
note = {Also research report 359, INRIA, 1979},
697
booktitle = {Computational Logic, Essays in Honor of
699
editor = {J.-L. Lassez and G. Plotkin},
700
publisher = {The MIT press},
705
author = {J. Ketonen and R. Weyhrauch},
706
journal = {Theoretical Computer Science},
708
title = {A decidable fragment of {P}redicate {C}alculus},
714
author = {S.C. Kleene},
715
publisher = {North-Holland},
716
series = {Bibliotheca Mathematica},
717
title = {Introduction to Metamathematics},
722
author = {J.-L. Krivine},
723
publisher = {Masson},
724
series = {Etudes et recherche en informatique},
725
title = {Lambda-calcul {types et mod\`eles}},
730
editor = {G. Huet and G. Plotkin},
731
publisher = {Cambridge University Press},
732
title = {Logical Environments},
737
editor = {G. Huet and G. Plotkin},
738
publisher = {Cambridge University Press},
739
title = {Logical Frameworks},
744
author = {A. Laville},
745
title = {Comparison of Priority Rules in Pattern
746
Matching and Term Rewriting},
747
journal = {Journal of Symbolic Computation},
753
@InProceedings{LePa94,
754
author = {F. Leclerc and C. Paulin-Mohring},
755
booktitle = {{Types for Proofs and Programs, Types' 93}},
756
editor = {H. Barendregt and T. Nipkow},
759
title = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
766
title = {The {ZINC} experiment: an economical implementation
767
of the {ML} language},
768
institution = {INRIA},
773
@InProceedings{Let02,
774
author = {P. Letouzey},
775
title = {A New Extraction for Coq},
778
crossref = {DBLP:conf/types/2002},
779
url = {draft at \url{http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz}}
784
title = {An Extended Calculus of Constructions},
785
school = {University of Edinburgh},
790
author = {{P. Martin-L\"of}},
791
publisher = {Bibliopolis},
792
series = {Studies in Proof Theory},
793
title = {Intuitionistic Type Theory},
798
author = {P. Manoury and M. Simonot},
799
title = {Automatizing Termination Proofs of Recursively Defined Functions.},
807
@InProceedings{Miquel00,
808
author = {A. Miquel},
809
title = {A Model for Impredicative Type Systems with Universes,
810
Intersection Types and Subtyping},
811
booktitle = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}},
812
publisher = {IEEE Computer Society Press},
816
@PhDThesis{Miquel01a,
817
author = {A. Miquel},
818
title = {Le Calcul des Constructions implicite: syntaxe et s\'emantique},
820
school = {{Universit\'e Paris 7}},
824
@InProceedings{Miquel01b,
825
author = {A. Miquel},
826
title = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping},
827
booktitle = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}},
834
@InProceedings{MiWer02,
835
author = {A. Miquel and B. Werner},
836
title = {The Not So Simple Proof-Irrelevant Model of CC},
840
ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm},
841
crossref = {DBLP:conf/types/2002},
842
bibsource = {DBLP, http://dblp.uni-trier.de}
845
@proceedings{DBLP:conf/types/2002,
846
editor = {H. Geuvers and F. Wiedijk},
847
title = {Types for Proofs and Programs, Second International Workshop,
848
TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
855
isbn = {3-540-14031-X},
856
bibsource = {DBLP, http://dblp.uni-trier.de}
859
@InProceedings{Moh89a,
860
author = {C. Paulin-Mohring},
862
booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
865
title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
870
author = {C. Paulin-Mohring},
872
school = {{Universit\'e Paris 7}},
873
title = {Extraction de programmes dans le {Calcul des Constructions}},
877
@InProceedings{Moh93,
878
author = {C. Paulin-Mohring},
879
booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications},
880
editor = {M. Bezem and J.-F. Groote},
881
note = {Also LIP research report 92-49, ENS Lyon},
885
title = {{Inductive Definitions in the System Coq - Rules and Properties}},
890
author = {C. Paulin-Mohring},
892
publisher = {{ENS Lyon}},
893
title = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}},
897
@MastersThesis{Mun94,
900
school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
901
title = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
906
author = {C. Mu{\~{n}}oz},
907
title = {Un calcul de substitutions pour la repr\'esentation
908
de preuves partielles en th\'eorie de types},
909
school = {Universit\'e Paris 7},
911
note = {Version en anglais disponible comme rapport de
912
recherche INRIA RR-3309},
913
type = {Th\`ese de Doctorat}
917
author = {B. {Nordstr\"om} and K. Peterson and J. Smith},
918
booktitle = {Information Processing 83},
919
publisher = {Oxford Science Publications},
920
series = {International Series of Monographs on Computer Science},
921
title = {Programming in {Martin-L\"of's} Type Theory},
926
author = {B. {Nordstr\"om}},
928
title = {Terminating General Recursion},
934
editor = {P. Odifreddi},
935
publisher = {Academic Press},
936
title = {Logic and Computer Science},
940
@InProceedings{PaMS92,
941
author = {M. Parigot and P. Manoury and M. Simonot},
942
address = {St. Petersburg, Russia},
943
booktitle = {Logic Programming and automated reasoning},
944
editor = {A. Voronkov},
949
title = {{ProPre : A Programming language with proofs}},
954
author = {C. Paulin-Mohring and B. Werner},
955
journal = {Journal of Symbolic Computation},
957
title = {{Synthesis of ML programs in the system Coq}},
963
author = {M. Parigot},
964
journal = {Theoretical Computer Science},
967
title = {{Recursive Programming with Proofs}},
972
@InProceedings{Parent95b,
973
author = {C. Parent},
974
booktitle = {{Mathematics of Program Construction'95}},
977
title = {{Synthesizing proofs from programs in
978
the Calculus of Inductive Constructions}},
983
@InProceedings{Prasad93,
984
author = {K.V. Prasad},
985
booktitle = {{Proceedings of CONCUR'93}},
988
title = {{Programming with broadcasts}},
994
author = {di~Cosmo, R.},
995
title = {Isomorphisms of Types: from $\lambda$-calculus to information
996
retrieval and language design},
997
series = {Progress in Theoretical Computer Science},
998
publisher = {Birkhauser},
1000
note = {ISBN-0-8176-3763-X}
1004
author = {J. Rouyer},
1005
institution = {INRIA},
1008
title = {{D�veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
1013
title = {Subtypes for Specifications: Predicate Subtyping in
1015
author = {John Rushby and Sam Owre and N. Shankar},
1016
journal = {IEEE Transactions on Software Engineering},
1024
@TechReport{Saibi94,
1025
author = {A. Sa\"{\i}bi},
1026
institution = {INRIA},
1029
title = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
1034
@MastersThesis{Ter92,
1035
author = {D. Terrasse},
1038
title = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
1042
@TechReport{ThBeKa92,
1043
author = {L. Th\'ery and Y. Bertot and G. Kahn},
1044
institution = {INRIA Sophia},
1047
title = {Real theorem provers deserve real user-interfaces},
1048
type = {Research Report},
1053
author = {A.S. Troelstra and D. van Dalen},
1054
publisher = {North-Holland},
1055
series = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
1056
title = {Constructivism in Mathematics, an introduction},
1061
author = {B. Werner},
1062
school = {Universit\'e Paris 7},
1063
title = {Une th\'eorie des constructions inductives},
1064
type = {Th\`ese de Doctorat},
1069
author = {B. Barras},
1070
school = {Universit\'e Paris 7},
1071
title = {Auto-validation d'un syst�me de preuves avec familles inductives},
1072
type = {Th\`ese de Doctorat},
1077
author = {D. de Rauglaudre},
1078
title = {Camlp4 version 1.07.2},
1080
note = {In Camlp4 distribution}
1084
author = {G. Dowek},
1085
title = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
1086
journal = {Journal Logic Computation},
1094
@InProceedings{manoury94,
1095
author = {P. Manoury},
1096
title = {{A User's Friendly Syntax to Define
1097
Recursive Functions as Typed $\lambda-$Terms}},
1098
booktitle = {{Types for Proofs and Programs, TYPES'94}},
1105
@TechReport{maranget94,
1106
author = {L. Maranget},
1107
institution = {INRIA},
1109
title = {{Two Techniques for Compiling Lazy Pattern Matching}},
1113
@InProceedings{puel-suarez90,
1114
author = {L.Puel and A. Su\'arez},
1115
booktitle = {{Conference Lisp and Functional Programming}},
1118
title = {{Compiling Pattern Matching by Term
1123
@MastersThesis{saidi94,
1124
author = {H. Saidi},
1126
school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
1127
title = {R\'esolution d'\'equations dans le syst\`eme T
1132
@inproceedings{sozeau06,
1133
author = {Matthieu Sozeau},
1134
title = {Subset Coercions in {C}oq},
1136
booktitle = {TYPES'06},
1139
publisher = "Springer",
1143
@inproceedings{sozeau08,
1144
Author = {Matthieu Sozeau and Nicolas Oury},
1145
booktitle = {TPHOLs'08},
1146
Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
1147
Title = {{F}irst-{C}lass {T}ype {C}lasses},
1151
@Misc{streicher93semantical,
1152
author = {T. Streicher},
1153
title = {Semantical Investigations into Intensional Type Theory},
1154
note = {Habilitationsschrift, LMU Munchen.},
1159
author = {Lemme Team},
1160
title = {Pcoq a graphical user-interface for {Coq}},
1161
note = {\url{http://www-sop.inria.fr/lemme/pcoq/}}
1165
author = {David Aspinall},
1166
title = {Proof General},
1167
note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
1171
title = {Interactive Theorem Proving and Program Development.
1172
Coq'Art: The Calculus of Inductive Constructions},
1173
author = {Yves Bertot and Pierre Cast�ran},
1174
publisher = {Springer Verlag},
1175
series = {Texts in Theoretical Computer Science. An EATCS series},
1179
@InCollection{wadler87,
1180
author = {P. Wadler},
1181
title = {Efficient Compilation of Pattern Matching},
1182
booktitle = {The Implementation of Functional Programming
1184
editor = {S.L. Peyton Jones},
1185
publisher = {Prentice-Hall},
1189
@inproceedings{DBLP:conf/types/CornesT95,
1190
author = {Cristina Cornes and
1192
title = {Automating Inversion of Inductive Predicates in Coq},
1193
booktitle = {TYPES},
1196
crossref = {DBLP:conf/types/1995},
1197
bibsource = {DBLP, http://dblp.uni-trier.de}
1199
@proceedings{DBLP:conf/types/1995,
1200
editor = {Stefano Berardi and
1202
title = {Types for Proofs and Programs, International Workshop TYPES'95,
1203
Torino, Italy, June 5-8, 1995, Selected Papers},
1204
booktitle = {TYPES},
1205
publisher = {Springer},
1206
series = {Lecture Notes in Computer Science},
1209
isbn = {3-540-61780-9},
1210
bibsource = {DBLP, http://dblp.uni-trier.de}
1213
@inproceedings{DBLP:conf/types/McBride00,
1214
author = {Conor McBride},
1215
title = {Elimination with a Motive},
1216
booktitle = {TYPES},
1219
ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
1220
crossref = {DBLP:conf/types/2000},
1221
bibsource = {DBLP, http://dblp.uni-trier.de}
1224
@proceedings{DBLP:conf/types/2000,
1225
editor = {Paul Callaghan and
1229
title = {Types for Proofs and Programs, International Workshop, TYPES
1230
2000, Durham, UK, December 8-12, 2000, Selected Papers},
1231
booktitle = {TYPES},
1232
publisher = {Springer},
1233
series = {Lecture Notes in Computer Science},
1236
isbn = {3-540-43287-6},
1237
bibsource = {DBLP, http://dblp.uni-trier.de}
1240
@Comment{cross-references, must be at end}
1243
editor = {B. Nordstr\"om and K. Petersson and G. Plotkin},
1244
publisher = {Available by ftp at site ftp.inria.fr},
1245
title = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
1250
editor = {H. Barendregt and T. Nipkow},
1253
title = {Types for Proofs and Programs},
1258
@article{ TheOmegaPaper,
1260
title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
1261
journal = "Communication of the ACM",
added
removed
doc/refman/biblio.bib
