| [1] |
John Allen.
Anatomy of Lisp.
McGraw-Hill Book Compagny, 1978. [ bib ] |
| [2] |
H. Barendregt.
Lambda Calculi with Types.
Technical Report 91-19, Catholic University Nijmegen, 1991.
in Handbook of Logic in Computer Science, Vol II. [ bib ] |
| [3] |
H. Barendregt.
Lambda calculi with types.
In Samson Abramsky, Dov Gabbay, and Tom S.E. Maibaum, editors,
Handbook of Logic in Computer Science, chapter 2.2. Oxford University
Press, 1992. [ bib ] |
| [4] |
The Objective Caml language.
http://pauillac.inria.fr/ocaml/. [ bib ] |
| [5] |
Daniel de Rauglaudre.
The Camlp4 Pre Processor.
http://caml.inria.fr/camlp4/. [ bib ] |
| [6] |
X. Leroy.
The Objective Caml system: Documentation and user's manual,
March 1997.
http://pauillac.inria.fr/ocaml/htmlman/. [ bib ] |
| [7] |
G. Castagna.
Surcharge, sous-typage et liaison tardive : fondements
fonctionnels de la programmation orientée objet.
Thèse de doctorat, Université Paris VII, Janvier 1994. [ bib ] |
| [8] |
Coq.
The Coq Proof Assistant, 2001.
http://coq.inria.fr/. [ bib ] |
| [9] |
G. Huet, G. Kahn, and C. Paulin-Mohring.
The Coq Proof Assistant Version 6.1, A Tutorial,
December 1996. [ bib ] |
| [10] |
T. 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. Springer-Verlag. [ bib ] |
| [11] |
T. Coquand and G. Huet.
The Calculus of Constructions.
Information and Computation, 76(2/3):95-120, 1988. [ bib ] |
| [12] |
T. Coquand.
Metamathematical Investigations of a Calculus of Constructions.
INRIA and Cambridge University, 1986. [ bib ] |
| [13] |
A. Church.
A set of postulates for the foundation of logic.
Annals of Mathematics, 2(33-34):346-366 and 839-864, 1932/33. [ bib ] |
| [14] |
A. Church.
A formulation of the simple theory of types.
Journal of Symbolic Logic, 5:56-68, 1940. [ bib ] |
| [15] |
A. Church.
The Calculi of Lambda Conversion.
Princeton University Press, 1941. [ bib ] |
| [16] |
Jean Goubault.
Implementing Functional Languages with Fast Equality, Sets and Maps:
an Exercise in Hash Consing.
In Journées Francophones des Langages Applicatifs
(JFLA'93), pages 222-238, Annecy, February 1993. [ bib | .ps.gz ] |
| [17] |
G. Gentzen.
Investigations into logical deduction.
In M. E. Szabo, editor, The collected papers of Gerhard
Gentzen. North Holland, 1969. [ bib ] |
| [18] |
H. Geuvers.
Logics and Type Systems.
PhD thesis, Catholic University Nijmegen, September 1993. [ bib ] |
| [19] |
E. Giménez.
Codifying guarded definitions with recursive schemes.
In Workshop on Types for Proofs and Programs, volume 996 of
Lecture Notes in Computer Science, pages 39-59. Springer-Verlag, 1994. [ bib ] |
| [20] |
E. Giménez.
An Application of Co-Inductive Types in Coq: Verification of the
Alternating Bit Protocol.
1995. [ bib | .ps.Z ] |
| [21] |
J.-Y. Girard.
Interprétation fonctionnelle et élimination des coupures de
l'arithmétique d'ordre supérieur.
Thèse de doctorat d'État, Univerité Paris 7, 1972. [ bib ] |
| [22] |
M. A. Harrison.
Introduction to Formal Language Theory.
Addison-Wesley, 1978. [ bib ] |
| [23] |
J. E. Hopcroft and J. D. Ullman.
Introduction to Automata Theory, Languages, and Computation.
Addison-Wesley, 1979. [ bib ] |
| [24] |
W. A. Howard.
The formulae-as-types notion of construction.
In Hindley and Seldin, editors, To H. B. Curry: Essays on
Combinatory Logic, Lambda-Calculus and Formalism, pages 479-490. Academic
Press, 1980. [ bib ] |
| [25] |
G. Huet and A. Saï bi.
Constructive category theory.
January 1995.
in CLICS-TYPES BRA meeting. [ bib ] |
| [26] |
G. Huet and A. Saïbi.
Constructive category theory.
To appear, 1996. [ bib ] |
| [27] |
M. P. Jones.
An introduction to Gofer, June 1995.
Draft version. [ bib ] |
| [28] |
S. C. Kleene and J. B. Rosser.
The inconsistency of certain formal logics.
Annals of Mathematics, 2(36):630-636, 1935. [ bib ] |
| [29] |
C. Kreitz.
Constructive Automata Theory Implemented with the Nuprl
Proof Development System.
Technical Report TR 86-779, Cornell University, Department of
Computer Science, September 1986. [ bib ] |
| [30] |
T. F. Melham.
The HOL finite_sets Library.
University of Cambridge, Computer Laboratory, February 1992. [ bib ] |
| [31] |
R.L. Constable et al.
Implementing Mathematics with the Nuprl Proof Development
System.
Prentice Hall, 1986. [ bib ] |
| [32] |
Chris Okasaki and Andrew Gill.
Fast Mergeable Integer Maps.
In Workshop on ML, pages 77-86, September 1998. [ bib | .ps.gz ] |
| [33] |
William Pugh.
The Omega Test: a fast and practical integer programming algorithm
for dependence analysis.
Communications of the ACM, 35(8):102-114, August 1992. [ bib ] |
| [34] |
C. Parent.
Developing certified programs in the system Coq - The
Program tactic.
Technical Report 93-29, École Normale Supérieure de Lyon,
October 1993.
Also in Proceedings of the BRA Workshop Types for Proofs and
Programs, May 93. [ bib ] |
| [35] |
C. Parent.
Synthèse de preuves de programmes dans le Calcul des
Constructions Inductives.
Thèse de doctorat, École Normale Supérieure de Lyon, Janvier
1995. [ bib ] |
| [36] |
C. Paulin-Mohring.
Extracting Fomega's programs from proofs in the Calculus of
Constructions.
In Sixteenth Annual ACM Symposium on Principles of Programming
Languages, Austin, January 1989. ACM. [ bib ] |
| [37] |
C. Paulin-Mohring.
Extraction de programmes dans le Calcul des Constructions.
Thèse de doctorat, Université de Paris VII, Janvier 1989. [ bib ] |
| [38] |
C. Paulin-Mohring.
Inductive definitions in the system coq.
Technical Report 92-49, LIP - ENS Lyon, 1993. [ bib ] |
| [39] |
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, volume 664 of
Lecture Notes in Computer Science. Springer-Verlag, 1993.
Also LIP research report 92-49. [ bib ] |
| [40] |
C. Paulin-Mohring and B. Werner.
Synthesis of ML programs in the system Coq.
Journal of Symbolic Computation, 15:607-640, 1993. [ bib ] |
| [41] |
Gordon D. Plotkin.
Call-by-Name, Call-by-Value and the lambda-Calculus.
Theoretical Computer Science, 1(2):125-159, 1975. [ bib ] |
| [42] |
D. Prawitz.
Natural deduction, a proof-theoretical study.
Almquist and Wiksell, 1965. [ bib ] |
| [43] |
A. Saïbi.
Une axiomatisation constructive de la théorie des catégories.
Technical report, INRIA, 1995.
To appear as a research report. [ bib ] |
| [44] |
Philip Wadler.
Views: A way for pattern matching to cohabit with data abstraction.
In 14th ACM Symposium on Principles of Programming Languages,
Munich, January 1987. [ bib ] |
| [45] |
B. Werner.
Une Théorie des Constructions Inductives.
Thèse de doctorat, Université de Paris VII, Mai 1994. [ bib ] |
| [46] |
David Lester.
Exact Arithmetic Implementations in Haskell and PVS proofs.
http://www.cs.man.ac.uk/arch/dlester/exact.html. [ bib ] |
| [47] |
H. Boehm, R. Cartwright, M. J. O'Donnell, and M. Riggle.
Exact Real Arithmetic: A Case Study in Higher Order Programming.
In Proceedings of the 1986 Lisp and Functional Programming
Conference, pages 162-173, 1986. [ bib ] |
| [48] |
Hans Boehm.
Exact Arithmetic Implementation in Java.
http://www.hpl.hp.com/personal/Hans_Boehm/crcalc/. [ bib ] |