References
-
[1]
-
David Aspinall.
Proof general.
https://proofgeneral.github.io/.
- [2]
-
Ph. Audebaud.
Partial Objects in the Calculus of Constructions.
In Proceedings of the sixth Conf. on Logic in Computer Science.
IEEE, 1991.
- [3]
-
Ph. Audebaud.
CC+ : an extension of the Calculus of Constructions with fixpoints.
In B. Nordström and K. Petersson and G. Plotkin, editor, Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages
21–34, 1992.
Also Research Report LIP-ENS-Lyon.
- [4]
-
Ph. Audebaud.
Extension du Calcul des Constructions par Points fixes.
PhD thesis, Université Bordeaux I, 1992.
- [5]
-
L. Augustsson.
Compiling Pattern Matching.
In Conference Functional Programming and Computer Architecture,
1985.
- [6]
-
H. Barendregt.
Lambda Calculi with Types.
Technical Report 91-19, Catholic University Nijmegen, 1991.
In Handbook of Logic in Computer Science, Vol II.
- [7]
-
H. Barendregt and T. Nipkow, editors.
Types for Proofs and Programs, volume 806 of Lecture Notes
in Computer Science.
Sprin-ger-Verlag, 1994.
- [8]
-
H.P. Barendregt.
The Lambda Calculus its Syntax and Semantics.
North-Holland, 1981.
- [9]
-
B. Barras.
Auto-validation d’un système de preuves avec familles
inductives.
Thèse de doctorat, Université Paris 7, 1999.
- [10]
-
J.L. Bates and R.L. Constable.
Proofs as Programs.
ACM transactions on Programming Languages and Systems, 7, 1985.
- [11]
-
M.J. Beeson.
Foundations of Constructive Mathematics, Metamathematical
Studies.
Sprin-ger-Verlag, 1985.
- [12]
-
G. Bellin and J. Ketonen.
A decision procedure revisited : Notes on direct logic, linear logic
and its implementation.
Theoretical Computer Science, 95:115–142, 1992.
- [13]
-
Stefano Berardi and Mario Coppo, editors.
Types for Proofs and Programs, International Workshop TYPES’95,
Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture
Notes in Computer Science. Springer, 1996.
- [14]
-
Yves Bertot and Pierre Castéran.
Interactive Theorem Proving and Program Development. Coq’Art:
The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS series. Springer
Verlag, 2004.
- [15]
-
E. Bishop.
Foundations of Constructive Analysis.
McGraw-Hill, 1967.
- [16]
-
Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire.
Full reduction at full throttle.
In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified
Programs and Proofs - First International Conference, CPP 2011, Kenting,
Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes
in Computer Science, pages 362–377. Springer, 2011.
- [17]
-
S. Boutin.
Certification d’un compilateur ML en Coq.
Master’s thesis, Université Paris 7, September 1992.
- [18]
-
S. Boutin.
Réflexions sur les quotients.
thèse d’université, Paris 7, April 1997.
- [19]
-
S. Boutin.
Using reflection to build efficient and certified decision procedure
s.
In Martin Abadi and Takahashi Ito, editors, TACS’97, volume
1281 of Lecture Notes in Computer Science. Sprin-ger-Verlag, 1997.
- [20]
-
R.S. Boyer and J.S. Moore.
A computational logic.
ACM Monograph. Academic Press, 1979.
- [21]
-
Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors.
Types for Proofs and Programs, International Workshop, TYPES
2000, Durham, UK, December 8-12, 2000, Selected Papers, volume 2277 of Lecture Notes in Computer Science. Springer, 2002.
- [22]
-
Laurent Chicli, Loïc Pottier, and Carlos Simpson.
Mathematical quotients and quotient types in coq.
In Geuvers and Wiedijk [66].
- [23]
-
R.L. Constable et al.
Implementing Mathematics with the Nuprl Proof Development
System.
Prentice-Hall, 1986.
- [24]
-
Th. Coquand.
Une Théorie des Constructions.
PhD thesis, Université Paris 7, January 1985.
- [25]
-
Th. Coquand.
An Analysis of Girard’s Paradox.
In Symposium on Logic in Computer Science, Cambridge, MA, 1986.
IEEE Computer Society Press.
- [26]
-
Th. Coquand.
Metamathematical Investigations of a Calculus of Constructions.
In P. Oddifredi, editor, Logic and Computer Science. Academic
Press, 1990.
INRIA Research Report 1088, also in [64].
- [27]
-
Th. Coquand.
A New Paradox in Type Theory.
In Proceedings 9th Int. Congress of Logic, Methodology and
Philosophy of Science, August 1991.
- [28]
-
Th. Coquand.
Pattern Matching with Dependent Types.
In Nordström et al. [116].
- [29]
-
Th. Coquand.
Infinite objects in Type Theory.
In H. Barendregt and T. Nipokow, editors, Types for Proofs and
Programs, volume 806 of Lecture Notes in Computer Science, pages
62–78. Sprin-ger-Verlag, 1993.
- [30]
-
Th. 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. Sprin-ger-Verlag.
- [31]
-
Th. Coquand and G. Huet.
Concepts Mathématiques et Informatiques formalisés dans le
Calcul des Constructions.
In The Paris Logic Group, editor, Logic Colloquium’85.
North-Holland, 1987.
- [32]
-
Th. Coquand and G. Huet.
The Calculus of Constructions.
Information and Computation, 76(2/3), 1988.
- [33]
-
Th. Coquand and C. Paulin-Mohring.
Inductively defined types.
In P. Martin-Löf and G. Mints, editors, Proceedings of
Colog’88, volume 417 of Lecture Notes in Computer Science.
Sprin-ger-Verlag, 1990.
- [34]
-
P. Corbineau.
A declarative language for the coq proof assistant.
In M. Miculan, I. Scagnetto, and F. Honsell, editors, TYPES ’07,
Cividale del Friuli, Revised Selected Papers, volume 4941 of Lecture
Notes in Computer Science, pages 69–84. Springer, 2007.
- [35]
-
C. Cornes.
Conception d’un langage de haut niveau de représentation de
preuves.
Thèse de doctorat, Université Paris 7, November 1997.
- [36]
-
Cristina Cornes and Delphine Terrasse.
Automating inversion of inductive predicates in coq.
In Berardi and Coppo [13], pages 85–104.
- [37]
-
J. Courant.
Explicitation de preuves par récurrence implicite.
Master’s thesis, DEA d’Informatique, ENS Lyon, September 1994.
- [38]
-
Haskell B. Curry, Robert Feys, and William Craig.
Combinatory Logic, volume 1.
North-Holland, 1958.
§9E.
- [39]
-
N.J. de Bruijn.
Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic
Formula Manipulation, with Application to the Church-Rosser Theorem.
Indag. Math., 34, 1972.
- [40]
-
N.J. de Bruijn.
A survey of the project Automath.
In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry : Essays
on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
- [41]
-
D. de Rauglaudre.
Camlp4 version 1.07.2.
In Camlp4 distribution, 1998.
- [42]
-
D. Delahaye.
Information retrieval in a coq proof library using type isomorphisms.
In Proceedings of TYPES ’99, Lökeberg, Lecture Notes in
Computer Science. Sprin-ger-Verlag, 1999.
- [43]
-
D. Delahaye.
A Tactic Language for the System Coq.
In Proceedings of Logic for Programming and Automated Reasoning
(LPAR), Reunion Island, volume 1955 of Lecture Notes in Computer
Science, pages 85–95. Sprin-ger-Verlag, November 2000.
- [44]
-
D. Delahaye and M. Mayero.
Field: une procédure de décision pour les nombres réels
en Coq.
In Journées Francophones des Langages Applicatifs,
Pontarlier. INRIA, Janvier 2001.
- [45]
-
R. di Cosmo.
Isomorphisms of Types: from λ-calculus to information
retrieval and language design.
Progress in Theoretical Computer Science. Birkhauser, 1995.
ISBN-0-8176-3763-X.
- [46]
-
G. Dowek.
Naming and scoping in a mathematical vernacular.
Research Report 1283, INRIA, 1990.
- [47]
-
G. Dowek.
Démonstration automatique dans le Calcul des Constructions.
PhD thesis, Université Paris 7, December 1991.
- [48]
-
G. Dowek.
L’indécidabilité du filtrage du troisième ordre dans les
calculs avec types dépendants ou constructeurs de types.
Compte-Rendus de l’Académie des Sciences, I,
312(12):951–956, 1991.
The undecidability of Third Order Pattern Matching in Calculi with
Dependent Types or Type Constructors.
- [49]
-
G. Dowek.
A second order pattern matching algorithm in the cube of typed
λ-calculi.
In Proceedings of Mathematical Foundation of Computer Science,
volume 520 of Lecture Notes in Computer Science, pages 151–160.
Sprin-ger-Verlag, 1991.
Also INRIA Research Report.
- [50]
-
G. Dowek.
A Complete Proof Synthesis Method for the Cube of Type Systems.
Journal Logic Computation, 3(3):287–315, June 1993.
- [51]
-
G. Dowek.
The undecidability of pattern matching in calculi where primitive
recursive functions are representable.
Theoretical Computer Science, 107(2):349–356, 1993.
- [52]
-
G. Dowek.
Third order matching is decidable.
Annals of Pure and Applied Logic, 69:135–155, 1994.
- [53]
-
G. Dowek.
Lambda-calculus, combinators and the comprehension schema.
In Proceedings of the second international conference on typed
lambda calculus and applications, 1995.
- [54]
-
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent,
C. Paulin-Mohring, and B. Werner.
The Coq Proof Assistant User’s Guide Version 5.8.
Technical Report 154, INRIA, May 1993.
- [55]
-
P. Dybjer.
Inductive sets and families in Martin-Löf’s type theory and their
set-theoretic semantics: An inversion principle for Martin-Löf’s type
theory.
In G. Huet and G. Plotkin, editors, Logical Frameworks,
volume 14, pages 59–79. Cambridge University Press, 1991.
- [56]
-
Roy Dyckhoff.
Contraction-free sequent calculi for intuitionistic logic.
The Journal of Symbolic Logic, 57(3), September 1992.
- [57]
-
J.-C. Filliâtre.
Une procédure de décision pour le calcul des prédicats direct.
Étude et implémentation dans le système Coq.
Master’s thesis, DEA d’Informatique, ENS Lyon, September 1994.
- [58]
-
J.-C. Filliâtre.
A decision procedure for direct predicate calculus.
Research report 96–25, LIP-ENS-Lyon, 1995.
- [59]
-
J.-C. Filliâtre.
Preuve de programmes impératifs en théorie des types.
Thèse de doctorat, Université Paris-Sud, July 1999.
- [60]
-
J.-C. Filliâtre.
Formal Proof of a Program: Find.
Submitted to Science of Computer Programming, January 2000.
- [61]
-
J.-C. Filliâtre and N. Magaud.
Certification of sorting algorithms in the system Coq.
In Theorem Proving in Higher Order Logics: Emerging Trends,
1999.
- [62]
-
J.-C. Filliâtre.
Verification of non-functional programs using interpretations in type
theory.
Journal of Functional Programming, 13(4):709–745, July 2003.
[English translation of [59]].
- [63]
-
E. Fleury.
Implantation des algorithmes de Floyd et de Dijkstra dans le
Calcul des Constructions.
Rapport de Stage, July 1990.
- [64]
-
Projet Formel.
The Calculus of Constructions. Documentation and user’s guide,
Version 4.10.
Technical Report 110, INRIA, 1989.
- [65]
-
Jean-Baptiste-Joseph Fourier.
Fourier’s method to solve linear inequations/equations systems.
Gauthier-Villars, 1890.
- [66]
-
H. Geuvers and F. 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.
Sprin-ger-Verlag, 2003.
- [67]
-
E. Giménez.
Codifying guarded definitions with recursive schemes.
In Types’94 : Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science. Sprin-ger-Verlag, 1994.
Extended version in LIP research report 95-07, ENS Lyon.
- [68]
-
E. Giménez.
An application of co-inductive types in coq: verification of the
alternating bit protocol.
In Workshop on Types for Proofs and Programs, number 1158 in
Lecture Notes in Computer Science, pages 135–152. Sprin-ger-Verlag, 1995.
- [69]
-
E. Giménez.
Un calcul des constructions infinies et son application á la
vérification de systèmes communicants.
PhD thesis, École Normale Supérieure de Lyon, 1996.
- [70]
-
E. Giménez.
A tutorial on recursive types in coq.
Technical report, INRIA, March 1998.
- [71]
-
E. Giménez and P. Castéran.
A tutorial on [co-]inductive types in coq.
available at http://coq.inria.fr/doc, January 2005.
- [72]
-
Alessandro Giovini, Teo Mora, Gianfranco Niesi, Lorenzo Robbiano, and Carlo
Traverso.
"one sugar cube, please" or selection strategies in the buchberger
algorithm.
In Proceedings of the ISSAC’91, ACM Press, pages 5–4, 1991.
- [73]
-
J.-Y. Girard.
Une extension de l’interprétation de Gödel à l’analyse, et
son application à l’élimination des coupures dans l’analyse et la
théorie des types.
In Proceedings of the 2nd Scandinavian Logic Symposium.
North-Holland, 1970.
- [74]
-
J.-Y. Girard.
Interprétation fonctionnelle et élimination des coupures de
l’arithmétique d’ordre supérieur.
PhD thesis, Université Paris 7, 1972.
- [75]
-
J.-Y. Girard, Y. Lafont, and P. Taylor.
Proofs and Types.
Cambridge Tracts in Theoretical Computer Science 7. Cambridge
University Press, 1989.
- [76]
-
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer.
How to make ad hoc proof automation less ad hoc.
SIGPLAN Not., 46(9):163–175, September 2011.
- [77]
-
Benjamin Grégoire and Xavier Leroy.
A compiled implementation of strong reduction.
In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings
of the Seventh ACM SIGPLAN International Conference on Functional
Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002.,
pages 235–246. ACM, 2002.
- [78]
-
John Harrison.
Metatheory and reflection in theorem proving: A survey and critique.
Technical Report CRC-053, SRI International Cambridge Computer
Science Research Centre,, 1995.
- [79]
-
D. Hirschkoff.
Écriture d’une tactique arithmétique pour le système Coq.
Master’s thesis, DEA IARFA, Ecole des Ponts et Chaussées, Paris,
September 1994.
- [80]
-
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.
- [81]
-
W.A. Howard.
The formulae-as-types notion of constructions.
In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry : Essays
on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
Unpublished 1969 Manuscript.
- [82]
-
G. Huet.
Programming of future generation computers.
In Proceedings of TAPSOFT87, volume 249 of Lecture Notes
in Computer Science, pages 276–286. Sprin-ger-Verlag, 1987.
- [83]
-
G. Huet.
Extending the calculus of constructions with type:type.
Unpublished, 1988.
- [84]
-
G. Huet.
Induction principles formalized in the Calculus of Constructions.
In K. Fuchi and M. Nivat, editors, Programming of Future
Generation Computers. Elsevier Science, 1988.
Also in [82].
- [85]
-
G. Huet, editor.
Logical Foundations of Functional Programming.
The UT Year of Programming Series. Addison-Wesley, 1989.
- [86]
-
G. Huet.
The Constructive Engine.
In R. Narasimhan, editor, A perspective in Theoretical Computer
Science. Commemorative Volume for Gift Siromoney. World Scientific
Publishing, 1989.
Also in [64].
- [87]
-
G. Huet.
The gallina specification language : A case study.
In Proceedings of 12th FST/TCS Conference, New Delhi, volume
652 of Lecture Notes in Computer Science, pages 229–240.
Sprin-ger-Verlag, 1992.
- [88]
-
G. Huet.
Residual theory in λ-calculus: a formal development.
J. Functional Programming, 4,3:371–394, 1994.
- [89]
-
G. Huet and J.-J. Lévy.
Call by need computations in non-ambigous linear term rewriting
systems.
In J.-L. Lassez and G. Plotkin, editors, Computational Logic,
Essays in Honor of Alan Robinson. The MIT press, 1991.
Also research report 359, INRIA, 1979.
- [90]
-
G. Huet and G. Plotkin, editors.
Logical Frameworks.
Cambridge University Press, 1991.
- [91]
-
G. Huet and G. Plotkin, editors.
Logical Environments.
Cambridge University Press, 1992.
- [92]
-
J. Ketonen and R. Weyhrauch.
A decidable fragment of Predicate Calculus.
Theoretical Computer Science, 32:297–307, 1984.
- [93]
-
S.C. Kleene.
Introduction to Metamathematics.
Bibliotheca Mathematica. North-Holland, 1952.
- [94]
-
J.-L. Krivine.
Lambda-calcul types et modèles.
Etudes et recherche en informatique. Masson, 1990.
- [95]
-
A. Laville.
Comparison of priority rules in pattern matching and term rewriting.
Journal of Symbolic Computation, 11:321–347, 1991.
- [96]
-
F. Leclerc and C. Paulin-Mohring.
Programming with Streams in Coq. A case study : The Sieve of
Eratosthenes.
In H. Barendregt and T. Nipkow, editors, Types for Proofs and
Programs, Types’ 93, volume 806 of LNCS. Sprin-ger-Verlag, 1994.
- [97]
-
Gyesik Lee and Benjamin Werner.
Proof-irrelevant model of CC with predicative induction and
judgmental equality.
Logical Methods in Computer Science, 7(4), 2011.
- [98]
-
X. Leroy.
The ZINC experiment: an economical implementation of the ML
language.
Technical Report 117, INRIA, 1990.
- [99]
-
P. Letouzey.
A new extraction for coq.
In Geuvers and Wiedijk [66].
- [100]
-
L.Puel and A. Suárez.
Compiling Pattern Matching by Term Decomposition.
In Conference Lisp and Functional Programming, ACM.
Sprin-ger-Verlag, 1990.
- [101]
-
Z. Luo.
An Extended Calculus of Constructions.
PhD thesis, University of Edinburgh, 1990.
- [102]
-
Sebastiaan P. Luttik and Eelco Visser.
Specification of rewriting strategies.
In 2nd International Workshop on the Theory and Practice of
Algebraic Specifications (ASF+SDF’97), Electronic Workshops in Computing.
Springer-Verlag, 1997.
- [103]
-
Assia Mahboubi and Enrico Tassi.
Canonical Structures for the working Coq user.
In Sandrine Blazy, Christine Paulin, and David Pichardie, editors,
ITP 2013, 4th Conference on Interactive Theorem Proving, volume 7998
of LNCS, pages 19–34, Rennes, France, 2013. Springer.
- [104]
-
P. Manoury.
A User’s Friendly Syntax to Define Recursive Functions as Typed
λ−Terms.
In Types for Proofs and Programs, TYPES’94, volume 996 of
LNCS, June 1994.
- [105]
-
P. Manoury and M. Simonot.
Automatizing termination proofs of recursively defined functions.
TCS, 135(2):319–343, 1994.
- [106]
-
L. Maranget.
Two Techniques for Compiling Lazy Pattern Matching.
Technical Report 2385, INRIA, 1994.
- [107]
-
Conor McBride.
Elimination with a motive.
In Callaghan et al. [21], pages 197–216.
- [108]
-
A. Miquel.
A model for impredicative type systems with universes, intersection
types and subtyping.
In Proceedings of the 15th Annual IEEE Symposium on Logic in
Computer Science (LICS’00). IEEE Computer Society Press, 2000.
- [109]
-
A. Miquel.
The implicit calculus of constructions: Extending pure type systems
with an intersection type binder and subtyping.
In Proceedings of the fifth International Conference on Typed
Lambda Calculi and Applications (TLCA01), Krakow, Poland, number 2044 in
LNCS. Sprin-ger-Verlag, 2001.
- [110]
-
A. Miquel.
Le Calcul des Constructions implicite: syntaxe et sémantique.
PhD thesis, Université Paris 7, dec 2001.
- [111]
-
A. Miquel and B. Werner.
The not so simple proof-irrelevant model of cc.
In Geuvers and Wiedijk [66], pages 240–258.
- [112]
-
C. Muñoz.
Un calcul de substitutions pour la représentation de preuves
partielles en théorie de types.
Thèse de doctorat, Université Paris 7, 1997.
Version en anglais disponible comme rapport de recherche INRIA
RR-3309.
- [113]
-
C. Muñoz.
Démonstration automatique dans la logique propositionnelle
intuitionniste.
Master’s thesis, DEA d’Informatique Fondamentale, Université Paris
7, September 1994.
- [114]
-
B. Nordström.
Terminating general recursion.
BIT, 28, 1988.
- [115]
-
B. Nordström, K. Peterson, and J. Smith.
Programming in Martin-Löf’s Type Theory.
International Series of Monographs on Computer Science. Oxford
Science Publications, 1990.
- [116]
-
B. Nordström, K. Petersson, and G. Plotkin, editors.
Proceedings of the 1992 Workshop on Types for Proofs and
Programs.
Available by ftp at site ftp.inria.fr, 1992.
- [117]
-
P. Odifreddi, editor.
Logic and Computer Science.
Academic Press, 1990.
- [118]
-
P. Martin-Löf.
Intuitionistic Type Theory.
Studies in Proof Theory. Bibliopolis, 1984.
- [119]
-
C. Parent.
Developing certified programs in the system Coq- The Program
tactic.
Technical Report 93-29, Ecole Normale Supérieure de Lyon,
October 1993.
Also in [7].
- [120]
-
C. Parent.
Synthèse de preuves de programmes dans le Calcul des
Constructions Inductives.
PhD thesis, Ecole Normale Supérieure de Lyon, 1995.
- [121]
-
C. Parent.
Synthesizing proofs from programs in the Calculus of Inductive
Constructions.
In Mathematics of Program Construction’95, volume 947 of LNCS. Sprin-ger-Verlag, 1995.
- [122]
-
M. Parigot.
Recursive Programming with Proofs.
Theoretical Computer Science, 94(2):335–356, 1992.
- [123]
-
M. Parigot, P. Manoury, and M. Simonot.
ProPre : A Programming language with proofs.
In A. Voronkov, editor, Logic Programming and automated
reasoning, number 624 in LNCS, St. Petersburg, Russia, July 1992.
Sprin-ger-Verlag.
- [124]
-
C. Paulin-Mohring.
Extracting Fω’s programs from proofs in the Calculus of
Constructions.
In Sixteenth Annual ACM Symposium on Principles of Programming
Languages, Austin, January 1989. ACM.
- [125]
-
C. Paulin-Mohring.
Extraction de programmes dans le Calcul des Constructions.
PhD thesis, Université Paris 7, January 1989.
- [126]
-
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, number 664 in LNCS.
Sprin-ger-Verlag, 1993.
Also LIP research report 92-49, ENS Lyon.
- [127]
-
C. Paulin-Mohring.
Le système Coq. Thèse d’habilitation.
ENS Lyon, January 1997.
- [128]
-
C. Paulin-Mohring and B. Werner.
Synthesis of ML programs in the system Coq.
Journal of Symbolic Computation, 15:607–640, 1993.
- [129]
-
K.V. Prasad.
Programming with broadcasts.
In Proceedings of CONCUR’93, volume 715 of LNCS.
Sprin-ger-Verlag, 1993.
- [130]
-
W. Pugh.
The omega test: a fast and practical integer programming algorithm
for dependence analysis.
Communication of the ACM, pages 102–114, 1992.
- [131]
-
J. Rouyer.
Développement de l’Algorithme d’Unification dans le Calcul des
Constructions.
Technical Report 1795, INRIA, November 1992.
- [132]
-
John Rushby, Sam Owre, and N. Shankar.
Subtypes for specifications: Predicate subtyping in PVS.
IEEE Transactions on Software Engineering, 24(9):709–720,
September 1998.
- [133]
-
A. Saïbi.
Axiomatization of a lambda-calculus with explicit-substitutions in
the Coq System.
Technical Report 2345, INRIA, December 1994.
- [134]
-
H. Saidi.
Résolution d’équations dans le système t de gödel.
Master’s thesis, DEA d’Informatique Fondamentale, Université Paris
7, September 1994.
- [135]
-
Matthieu Sozeau.
Subset coercions in Coq.
In TYPES’06, volume 4502 of LNCS, pages 237–252.
Springer, 2007.
- [136]
-
Matthieu Sozeau and Nicolas Oury.
First-Class Type Classes.
In TPHOLs’08, 2008.
- [137]
-
T. Streicher.
Semantical investigations into intensional type theory, 1993.
Habilitationsschrift, LMU Munchen.
- [138]
-
Lemme Team.
Pcoq a graphical user-interface for Coq.
http://www-sop.inria.fr/lemme/pcoq/.
- [139]
-
The Coq Development Team.
The Coq Proof Assistant Reference Manual Version 7.2.
Technical Report 255, INRIA, February 2002.
- [140]
-
D. Terrasse.
Traduction de TYPOL en COQ. Application à Mini ML.
Master’s thesis, IARFA, September 1992.
- [141]
-
L. Théry, Y. Bertot, and G. Kahn.
Real theorem provers deserve real user-interfaces.
Research Report 1684, INRIA Sophia, May 1992.
- [142]
-
A.S. Troelstra and D. van Dalen.
Constructivism in Mathematics, an introduction.
Studies in Logic and the foundations of Mathematics, volumes 121 and
123. North-Holland, 1988.
- [143]
-
P. Wadler.
Efficient compilation of pattern matching.
In S.L. Peyton Jones, editor, The Implementation of Functional
Programming Languages. Prentice-Hall, 1987.
- [144]
-
P. Weis and X. Leroy.
Le langage Caml.
InterEditions, 1993.
- [145]
-
B. Werner.
Une théorie des constructions inductives.
Thèse de doctorat, Université Paris 7, 1994.
