References
-
[Acz99]
-
Peter Aczel.
On relating type theories and set theories.
In Types’98. Springer Verlag, 1999.
- [BBC+99]
-
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann
Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre,
Eduardo Giménez, Hugo Herbelin, Gérard Huet, Henri Laulhère,
Cesar Muñoz, Chetan Murthy, Catherine Parent-Vigouroux, Patrick
Loiseleur, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin
Werner.
The Coq proof assistant — reference manual.
Disponible en http://coq.inria.fr/doc/main.html., décembre
1999.
Version 6.3.1.
- [Coq94]
-
Thierry Coquand.
A new paradox in type theory.
In D. Prawitz, B. Skyrms, and D. Westerståhl, editors, Proceedings 9th International Congress of Logic, Methodology and Philosophy
of Science, Uppsala, Suède, 7–14 août 1991, volume 134 of Studies
in Logic and the Foundations of Mathematics, pages 555–570. North-Holland,
Amsterdam, avril 1994.
Disponible en
http://hypatia.dcs.qmw.ac.uk/data/C/CoquandTFH/nyparadox.ps.Z.
- [DHK98]
-
Gilles Dowek, Thérèse Hardin, and Claude Kirchner.
Theorem proving modulo.
Technical Report RR-3400, Inria, Institut National de Recherche en
Informatique et en Automatique, avril 1998.
Disponible en http://www.inria.fr/RRRT/RR-3400.html.
- [FFKD87]
-
Matthias Felleisen, Daniel P. Friedman, Emil Kohlbecker, and Bruce Duba.
A syntactic theory of sequential control.
Theoretical Computer Science, 52(3):205–237, 1987.
- [Fri78]
-
Harvey Friedman.
Classically and intuitionistically provably recursive functions.
In D. S. Scott and G. H. Muller, editors, Higher Set Theory,
volume 699 of Lecture Notes in Mathematics, pages 21–28. Springer
Verlag, 1978.
- [GLT89]
-
Jean-Yves Girard, Yves Lafont, and Paul Taylor.
Proofs and Types, volume 7 of Cambridge Tracts in
Theoretical Computer Science.
Cambridge University Press, 1989.
- [Gri90]
-
Timothy G. Griffin.
A formulas-as-types notion of control.
In Proceedings of the 17th Annual ACM Symposium on Principles
of Programming Languages, pages 47–58, San Francisco, California, janvier
1990.
- [HHP87]
-
Robert Harper, Furio Honsell, and Gordon Plotkin.
A framework for defining logics.
In Symposium on Logic in Computer Science, Ithaca, NY, pages
194–204. IEEE, June 1987.
- [HMT90]
-
Robert Harper, Robin Milner, and Mads Tofte.
The Definition of Standard ML.
MIT Press, 1990.
- [Joh87]
-
Peter T. Johnstone.
Notes on Logic and Set Theory.
Cambridge University Press, 1987.
- [Koh98]
-
Ulrich Kohlenbach.
Proof interpretations.
Cours de doctorat, BRICS, Danemark. Disponible en
http://www.brics.dk/~kohlenb/file.ps, 1998.
- [MNPS91]
-
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.
Uniform proofs as a foundation for logic programming.
Annals of Pure and Applied Logic, 51:125–157, 1991.
Disponible en
ftp://ftp.cis.upenn.edu/pub/papers/miller/apal91.dvi.Z, errata en
ftp://ftp.cis.upenn.edu/pub/papers/miller/apal91-errata.dvi.
- [Par92]
-
Michel Parigot.
λµ-calculus: an algorithmic interpretation of classical
natural deduction.
In 3rd International Conference on Logic Programming and
Automated Reasoning, volume 417 of Lecture Notes in Computer Science,
Saint-Petersburg, USSR, juillet 1992. Springer Verlag.
- [PH78]
-
Jeff Paris and Leo Harrington.
A mathematical incompleteness of Peano Arithmetic.
In Jon Barwise, editor, Handbook of Mathematical Logic, chapter
D.8, pages 1133–1142. North-Holland, Amsterdam, second edition, 1978.
- [Plo76]
-
Gordon Plotkin.
Call-by-name, call-by-value and the λ-calculus.
Theoretical Computer Science, 1(1):125–159, 1976.
- [Rég94]
-
Laurent Régnier.
Une équivalence sur les lambda-termes.
Theoretical Computer Science, 126, 1994.
Disponible en
http://hypatia.dcs.qmw.ac.uk/data/R/RegnierL/sigma.ps.gz.
- [Wer97]
-
Benjamin Werner.
Sets in types, types in sets.
In Martin Abadi and Takahashi Ito, editors, TACS’97, volume
1281. LNCS, Springer-Verlag, 1997.
Disponible en
http://pauillac.inria.fr/~werner/publis/zfc.ps.gz, fichier Coq en
http://pauillac.inria.fr/~werner/ZFC.v.