Previous Up

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, Hndbo/k mf 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.

Previous Up