Références
-
[Arg98]
-
Pablo Argon.
Etude sur l’application de méthodes formelles à la
compilation et à la validation de programmes Electre.
Thèse de doctorat, École Centrale de Nantes, 1998.
- [AVL62]
-
G. M. Adel’son-Vel’skiĭ and E. M. Landis.
An algorithm for the organization of information.
Soviet Mathematics–Doklady, 3(5):1259–1263, September 1962.
- [Bal02]
-
Antonia Balaa.
Fonctions récursives générales dans le calcul des
constructions.
Thèse de doctorat, Université de Nice – Sophia-Antipolis, November
2002.
- [Bar81]
-
Henk P. Barendregt.
The Lambda Calculus its Syntax and Semantics.
North-Holland, 1981.
- [BB95]
-
Stefano Berardi and Luca Boerio.
Using subtyping in program optimization.
In Typed Lambda Calculus and Applications, 1995.
- [BB96]
-
Franco Barbanera and Stefano Berardi.
Proof-irrelevance out of excluded-middle and choice in the calculus
of constructions.
Journal of Functional Programming, 6(3):519–525, 1996.
- [BC04]
-
Yves Bertot and Pierre Castéran.
Interactive Theorem Proving and Program Development.
Texts in Theoretical Computer Science. An EATCS Series. Springer
Verlag, 2004.
http://www.labri.fr/Perso/~casteran/CoqArt/index.html.
- [Bee85]
-
Michael J. Beeson.
Foundations of Constructive Mathematics, Metamathematical
Studies.
Springer-Verlag, 1985.
- [Ber96]
-
Stefano Berardi.
Pruning simply typed lambda terms.
Journal of Logic and Computation, 6(5):663–681, 1996.
- [Ber98]
-
Yves Bertot.
A certified compiler for an imperative language.
Rapport de Recherche RR-34-88, INRIA, 1998.
- [CDDK86]
-
Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, and Gilles Kahn.
A simple applicative language: Mini-ML.
Rapport de Recherche 529, INRIA, May 1986.
- [Chr03a]
-
Jacek Chrząszcz.
Implementing modules in the system Coq.
In 16th International Conference on Theorem Proving in Higher
Order Logics, University of Rome III, September 2003.
- [Chr03b]
-
Jacek Chrząszcz.
Modules in Type Theory with generative definitions.
PhD thesis, Warsaw University and Université Paris-Sud, 2003.
To be defended.
- [Coq]
-
Catarina Coquand.
Agda.
http://www.cs.chalmers.se/~catarina/agda/.
- [Coq85]
-
Thierry Coquand.
Une Théorie des Constructions.
PhD thesis, Université Paris 7, January 1985.
- [Coq86]
-
Thierry Coquand.
An analysis of girard’s paradox.
In Symposium on Logic in Computer Science, Cambridge, MA, 1986.
IEEE Computer Society Press.
- [Coq94a]
-
Thierry Coquand.
Infinite objects in type theory.
In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs
and Programs, volume 806 of LNCS, pages 62–78. Springer-Verlag, 1994.
- [Coq94b]
-
Thierry Coquand.
A new paradox in type theory.
In 9th International Conference on Logic, Methodology, and
Philosophy of Science, pages 555–570, 1994.
- [Coq07]
-
The Coq Development Team.
The Coq Proof Assistant Reference Manual.
INRIA, 2007.
Version 8.1, available at http://coq.inria.fr/doc/main.html.
- [Cou90]
-
Patrick Cousot.
Methods and logics for proving programs.
In J. van Leeuwen, editor, Handbook of Theoretical Computer
Science, volume B, pages 841–993. North-Holland, 1990.
- [CPM90]
-
Thierry Coquand and Christine Paulin-Mohring.
Inductively defined types.
In P. Martin-Löf and G. Mints, editors, Proceedings of
Colog’88. Springer-Verlag, 1990.
LNCS 417.
- [Dia75]
-
Radu Diaconescu.
Axiom of choice and complementation.
In Proceedings of AMS, volume 51, pages 176–178, 1975.
- [Dij76]
-
Edsger W. Dijkstra.
A discipline of programming.
Series in Automatic Computation. Prentice Hall Int., 1976.
- [DP98]
-
Ferrucio Damiani and Frédéric Prost.
Detecting and removing dead-code using rank 2 intersection.
In Proceedings TYPES’96, LNCS, 1998.
- [Fil99]
-
Jean-Christophe Filliâtre.
Preuve de programmes impératifs en théorie des types.
Thèse de doctorat, Université Paris-Sud, July 1999.
- [Fil02]
-
Jean-Christophe Filliâtre.
The why verification tool, 2002.
http://why.lri.fr/.
- [Fil03a]
-
Jean-Christophe Filliâtre.
Verification of Non-Functional Programs using Interpretations in
Type Theory.
Journal of Functional Programming, 13(4):709–745, July 2003.
- [Fil03b]
-
Jean-Christophe Filliâtre.
Why: a multi-language multi-prover verification tool.
Research Report 1366, LRI, Université Paris Sud, March 2003.
http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz.
- [FL04]
-
Jean-Christophe Filliâtre and Pierre Letouzey.
Functors for Proofs and Programs.
In Proceedings of The European Symposium on Programming,
Barcelona, Spain, March 29-April 2 2004.
Voir aussi http://www.lri.fr/~filliatr/fsets/.
- [Geu01]
-
Herman Geuvers.
Induction is not derivable in second order dependent type theory.
In TLCA, pages 166–181, 2001.
- [Gim95]
-
Eduardo Giménez.
Codifying guarded definitions with recursive schemes.
In P. Dybjer, B. Nordström, and J. Smith, editors, Types for
Proofs and Programs, TYPES’94, volume 996 of LNCS, pages 39–59.
Springer-Verlag, 1995.
- [Gim96a]
-
Eduardo Giménez.
An application of co-inductive types in Coq : Verification of the
alternating bit protocol.
In Stefano Berardi and Mario Coppo, editors, Types for Proofs
and Programs, TYPES’95, volume 1158 of LNCS, 1996.
- [Gim96b]
-
Eduardo Giménez.
Un Calcul de Constructions Infinies et son application à la
vérification de systèmes communicants.
Thèse d’université, Ecole Normale Supérieure de Lyon, December 1996.
- [Gim97]
-
Eduardo Giménez.
A certification of Petersson’s algorithm for managing mutual
exclusion.
Coq’s Contributions, 1997.
- [Gim98]
-
Eduardo Giménez.
A tutorial on recursive types in coq.
Rapport Technique 0221, INRIA, May 1998.
- [Gir72]
-
Jean-Yves Girard.
Interprétation fonctionnelle et élimination des coupures de
l’arithmétique d’ordre supérieur, 1972.
- [Gro]
-
Computer Assisted Reasoning Group.
The PLASTIC proof assistant.
http://www.dur.ac.uk/CARG/plastic.html.
- [Her05]
-
Hugo Herbelin.
On the degeneracy of sigma-types in presence of computational
classical logic.
In Pawel Urzyczyn, editor, Seventh International Conference,
TLCA ’05, Nara, Japan. April 2005, Proceedings, volume 3461 of LNCS,
pages 209–220. Springer, 2005.
- [HS98]
-
Martin Hofmann and Thomas Streicher.
The groupoid interpretation of type theory.
In Proceedings of the meeting Twenty-five years of constructive
type theory. Oxford University Press, 1998.
- [Kle45]
-
Stephen C. Kleene.
On the interpretation of intuitionistic number theory.
The Journal of Symbolic Logic, 10:109–124, 1945.
- [Kle98]
-
Thomas Kleymann.
Hoare Logic and VDM: Machine-Checked Soundness and Completeness
Proofs.
PhD thesis, Edinburgh-LFCS-Technical Report ECS-LFCS-98-392, 1998.
- [Ler00]
-
Xavier Leroy.
A modular module system.
Journal of Functional Programming, 10(3):269–303, 2000.
- [Let03a]
-
Pierre Letouzey.
A New Extraction for Coq.
In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs
and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The
Netherlands, April 24-28, 2002, volume 2646 of Lecture Notes in
Computer Science. Springer-Verlag, 2003.
- [Let03b]
-
Pierre Letouzey.
Programmation fonctionnelle certifiée en Coq.
PhD thesis, Université Paris Sud, 2003.
To be defended.
- [Luo90]
-
Zhaohui Luo.
An Extended Calculus of Constructions.
PhD thesis, University of Edinburgh, 1990.
- [LW99]
-
Samuel Lacas and Benjamin Werner.
Which choices imply the excluded middle?
manuscript, 1999.
- [McB99]
-
Conor McBride.
Dependently Typed Functional Programs and their Proofs.
Phd thesis, Université d’Édimbourg, 1999.
- [Miq01]
-
Alexandre Miquel.
Le calcul des constructions implicite : syntaxe et
sémantique.
PhD thesis, Université Paris 7, December 2001.
- [MPMU04]
-
Claude Marché, Christine Paulin-Mohring, and Xavier Urbain.
The Krakatoa tool for certification of
Java/JavaCard programs annotated in JML.
Journal of Logic and Algebraic Programming, 58(1–2):89–106,
2004.
http://krakatoa.lri.fr.
- [MW98]
-
Paul-André Melliès and Benjamin Werner.
A generic normalisation proof for pure type systems.
In Eduardo Giménez and Christine Paulin-Mohring, editors, Types for Proofs and Programs, International Workshop TYPES’96, Aussois,
France, December 15-19, 1996, Selected Papers, volume 1512 of Lecture
Notes in Computer Science, pages 254–276. Springer, 1998.
- [MW03]
-
Alexandre Miquel and Benjamin Werner.
The not so simple proof-irrelevant model of cc.
In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs
and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The
Netherlands, April 24-28, 2002, Selected Papers, volume 2646 of Lecture
Notes in Computer Science, pages 240–258. Springer, 2003.
- [PM89a]
-
Christine Paulin-Mohring.
Extracting Fω’s programs from proofs in the Calculus of
Constructions.
In Association for Computing Machinery, editor, Sixteenth Annual
ACM Symposium on Principles of Programming Languages, Austin, January 1989.
- [PM89b]
-
Christine Paulin-Mohring.
Extraction de programmes dans le Calcul des Constructions.
PhD thesis, Université Paris 7, January 1989.
- [Poi02]
-
Henri Poincaré.
La Science et l’Hypothèse.
Flammarion, 1902.
- [Pol]
-
Randy Pollack.
The LEGO proof assistant.
http://www.dcs.ed.ac.uk/home/lego/.
- [PS]
-
Frank Pfenning and Carsten Schürmann.
The Twelf project.
http://www-2.cs.cmu.edu/~twelf/.
- [Raf]
-
Christophe Raffalli.
The PhoX proof assistant.
http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web/RAFFALLI/af2.%
html.
- [Sch97]
-
Thomas Schreiber.
Auxiliary variables and recursive procedures.
In TAPSOFT’97, volume 1214 of LNCS, pages 697–711, 1997.
- [SG95]
-
Milena Stefanova and Herman Geuvers.
A simple model construction for the calculus of constructions.
In TYPES, volume 1158 of Lecture Notes in Computer
Science, pages 249–264. Springer, 1995.
- [Tak91]
-
Yukihide Takayama.
Extraction of redundancy-free programs from constructive natural
deduction proofs.
Journal of Symbolic Computation, 12:29–69, 1991.
- [Ter92]
-
Delphine Terrasse.
Traduction de TYPOL en COQ. Application à Mini ML.
Rapport de dea, IARFA, September 1992.
- [Tro73]
-
Anne S. Troelstra, editor.
Metamathematical Investigation of Intuitionistic Arithmetic and
Analysis.
LNM 344. Springer-Verlag, 1973.
- [TvD88]
-
Anne S. Troelstra and Dirk van Dalen.
Constructivism in Mathematics, an introduction.
Studies in Logic and the foundations of Mathematics, volumes 121 and
123. North-Holland, 1988.
- [VGLPAK00]
-
Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, and S. Arun-Kumar.
Reflecting BDDs in Coq.
In ASIAN’2000, volume 1961 of LNCS, pages 162–181, 2000.
- [Wer94]
-
Benjamin Werner.
Une théorie des constructions inductives.
Thèse de doctorat, Université Paris 7, 1994.
- [Wiea]
-
Freek Wiedijk.
Comparing mathematical provers.
http://www.cs.kun.nl/~freek/comparison/index.html.
- [Wieb]
-
Freek Wiedijk.
The fifteen provers of the world.
http://www.cs.kun.nl/~freek/comparison/index.html.