## Abstract

The calculus of constructions of Coquand, which is a version of higher order typed*λ*-calculus based on the dependent function type, is considered from the perspective of its use as the mathematical foundation for a proof development system. The paper considers formulations of the calculus, the underlying consistency of the formalism (i.e., the strong normalisation theorem), and the proof theory of adding assumptions for notions from logic and set theory. Proofs are not given, but references to them are.

This is a preview of subscription content, access via your institution.

## References

- [And65]
Andrews, P. B.:

*A Transfinite Type Theory with Type Variables*. North-Holland Publishing Company, Amsterdam, 1965. - [Con86]
Constable, R. et al.:

*Implementing Mathematics with the Nuprl Proof Development System*. Prentice-Hall, Englewood Cliffs, NJ, 1986. - [CoH86a]
Coquand, T. and Huet, G.: Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions. In:

*Logic Colloquium '85: Proceedings of the Colloquium Held in Orsay, July 7–13, 1985*, Ch. Berline, E. Bouscaren, M. Dickmann, J.-L. Krivine, D. Lascar, M. Parigot, E. Pelz and G. Sabbagh, (eds), Vol. 122 Studies in Logic and the Foundations of Mathematics, pp. 123–146, Amsterdam and New York, 1986. North-Holland. - [CoH86b]
Coquand, T. and Huet, G.: Constructions: A Higher Order Proof System for Mechanizing Mathematics. In

*EUROCAL85*, Vol. 203 Lecture Notes in Computer Science, pp. 151–184, Springer-Verlag, Berlin, 1986. - [CoH88]
Coquand, T. and Huet, G.: The Calculus of Constructions.

*Information and Computation*,**76**, 95–120 (1988). - [Coq85]
Coquand, T.: Une Théorie des Constructions. PhD Thesis, University of Paris VII, 1985.

- [Coq86]
Coquand, T.: An Analysis of Girard's Paradox. In:

*Symp. on Logic in Computer Science*, pp. 227–236. IEEE Computer Society, IEEE Computer Society Press, 1986. - [Coq87]
Coquand, T.: Metamathematical Investigations of a Calculus of Constructions. February 9, 1987. Privately circulated, 1987.

- [Cur63]
Curry, H. B.:

*Foundations of Mathematical Logic*. McGraw-Hill Book Company, New York, San Francisco, Toronto, and London, 1963. Reprinted by Dover, 1977 and 1984. - [CuF58]
Curry, H. B. and Feys, R.:

*Combinatory Logic*, Vol. 1. North-Holland Publishing Company, Amsterdam, 1958. Reprinted 1968 and 1974. - [CHS72]
Curry, H. B., Hindley, J. R. and Seldin, J. P.:

*Combinatory Logic*, volume 2. North-Holland Publishing Company, Amsterdam and London, 1972. - [Daa80]
Daalen, D. T. van: The Language Theory of AUTOMATH. PhD Thesis, Technische Hogeschool Eindhoven, February 1980.

- [dBr72]
De Bruijn, N. G.: Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation with Application to the Church-Rosser Theorem.

*Indagationes Mathematicae*,**34**, 381–392 (1972). - [Fit52]
Fitch, F. B.:

*Symbolic Logic*. The Ronald Press Company, New York, 1952. - [Gir72]
Girard, J.-Y.: Interprétation Fonctionnelle et Élimination des Coupures de L'Arithmétique d'Orde Supérieur. PhD Thesis, University of Paris VII, 1972.

- [HiS86]
Hindley, J. R. and Seldin, J. P.:

*Introduction to Combinators and λ-calculus*. Cambridge University Press, 1986. - [How80]
Howard, W. A.: The Formulae-as-types Notion of Construction. In:

*To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, J. R. Hindley and J. P. Seldin, (eds), pp. 479–490. Academic Press, New York, 1980. A version of this paper was privately circulated in 1969. - [Hue86]
Huet, G.: Formal Structures for Computation and Deduction. Course Notes, Carnegie-Mellon University, First Edition, May 1986.

- [Hue87]
Huet, G.: Induction Principles Formalized in the Calculus of Constructions. In:

*TAPSOFT '87: Proc. International Joint Conf. on Theory and Practice of Software Development, Pisa, Italy, March 23–27, 1987. Vol. 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP '87)*, H. Ehrig, R. Kowalski, G. Levi and U. Montanari, (eds), Vol. 249 Lecture Notes in Computer Science, pp. 276–286, Springer-Verlag, Berlin, 1987. - [KDE88a]
Korelsky, T., Dean, W., Eichenlaub, C., Hook, J., Klapper, C., Lam, M., McCullough, D, Brooke-McFarland, C., Pottinger, G., Rambow, O., Rosenthal, D., Seldin, J. P. and Weber, D. G.: Ulysses: A Computer-Security Modeling Environment. In

*Proc. 11th National Computer Security Conf., Baltimore, Maryland, October 17–20, 1988*, pp. 20–28. National Bureau of Standards and National Computer Security Center, October 1988. - [KDE88b]
Korelsky, T., Dean, W., Eichenlaub, C., Hook, J., Klapper, C., Lam, M., McCullough, D., Pottinger, G., Rambow, O., Rosenthal, D., Seldin, J. P. and Weber, D.G.: Security Modelling in the Ulysses Environment. In

*Proc. Fourth Aerospace Computer Security Applications Conf. Orlando, Florida, December 12–16, 1988*, pp. 386–392. IEEE Computer Society Press, December 1988. - [Luo89]
Luo, Z.: ECC, an Extended Calculus of Constructions. In

*Proc. Fourth Annual Symp. on Logic in Computer Science, June 1989, Asilomar, California, USA*, 1989. - [Luo90]
Luo, Z.: An Extended Calculus of Constructions. PhD Thesis, University of Edinburgh, 1990.

- [Mar71]
Martin-Löf, P.: A Theory of Types. Revised October 1971. Privately circulated, February 1971.

- [Mar75]
Martin-Löf, P.: An Intuitionistic Theory of Types: Predicative Part. In:

*Logic Colloquium '73*, H. E. Rose and J. C. Shepherdson (eds), pp. 73–118. North-Holland Publishing Company, Amsterdam, 1975. - [Mar82]
Martin-Löf, P.: Constructive Mathematics and Computer Science. In:

*Logic, Methodology and Philosophy of Science VI*, L. J. Cohen, J. Los, H. Pfeiffer and K.-P. Podewski (eds), pp. 153–175. North-Holland Publishing Company, Amsterdam, 1982. - [Mar84]
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Naples, 1984. Notes by G. Sambin of a series of lectures given in Padua, June 1980.

- [Ned73]
Nederpelt, R. P.: Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types. PhD Thesis, Technical University of Eindhoven, 1973.

- [Pot87]
Pottinger, G.: Strong Normalization for Terms of the Theory of Constructions. Technical Report TR 11-7, Odyssey Research Associates, December 1987.

- [Pot90]
Pottinger, G.: A tour of the multivariate lambda Calculus. In:

*Truth or Consequences: Essays in Honor of Nuel Belnap*, J. M. Dunn and A. Gupta (eds), pp. 209–229. Kluwer Academic Publishers, Dordrecht, Boston, and London, 1990. - [Pra65]
Prawitz, D.:

*Natural Deduction*. Almqvist & Wiksell, Stockholm, Göteborg and Uppsala, 1965. - [Sel77]
Seldin, J. P.: A Sequent Calculus for Type Assignment.

*Journal of Symbolic Logic*,**42**, 11–28 (1977). - [Sel87]
Seldin, J. P.: MATHESIS: The Mathematical Foundation for ULYSSES. Interim Report RADC-TR-87-223, RADC, November 1987. (Published 1988.)

- [Sel91]
Seldin, J. P.: Excluded Middle Without Definite Descriptions in the Theory of Constructions. Extended Abstract.

*Proc. of the First Montréal Workshop on Programming Language Theory*, Concordia University, Montréal, April 29–30, 1991, M. Okada and P. J. Scott (eds), pp. 74–83 Concordia University Centre for Pattern Recognition and Machine Intelligence Montréal, 1991. - [Sel]
Seldin, J. P.: On the Proof Theory of Coquand's Calculus of Constructions. In preparation.

## Author information

### Affiliations

### Corresponding author

## Rights and permissions

## About this article

### Cite this article

Seldin, J.P. Coquand's calculus of constructions: A mathematical foundation for a proof development system.
*Formal Aspects of Computing* **4, **425–441 (1992). https://doi.org/10.1007/BF01211392

Received:

Accepted:

Issue Date:

### Keywords

- Typed lambda calculus
- Higher order logic
- Strong normalisation theorem
- Consistency of assumptions