×

zbMATH — the first resource for mathematics

The calculus of constructions. (English) Zbl 0654.03045
This paper presents a calculus which is an impredicative extension of Martin-Löf type theory. It contains as a subsystem the functional system \(F\omega\) developed by J. Y. Girard (1972) in order to extend Gödel’s Dialectica interpretation to higher-order arithmetic. It has been shown since then [in Ch. Paulin’s thesis (Paris VIII, 1989)] how to define a modified realizability interpretation from the present calculus in \(F\omega\), and hence that the calculus of construction is conservative over \(F\omega\).
The notation used is that of Automath and the system is suitable for implementation, and can be seen as a very general type system for functional programming language and/or mechanized mathematics. A realizability interpretation in untyped \(\lambda\)-calculus is described. This has been generalized to an extensional model of the calculus using the notion of \(\omega\)-sets of E. Moggi, in Th. Ehrhard’s thesis (Paris VII, 1988) and in Th. Streicher’s thesis (Passau, 1988).
Reviewer: T.Coquand

MSC:
03F35 Second- and higher-order arithmetic and fragments
03B40 Combinatory logic and lambda calculus
68N01 General topics in the theory of software
Software:
Automath
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barendregt, H., ()
[2] Barendregt, H.; Rezus, A., Semantics for classical AUTOMATH and related systems, Inform. and control, 59, 127-147, (1983) · Zbl 0564.68060
[3] de Bruijn, N.G., The mathematical language AUTOMATH, its usage and some of its extensions, (), 29-61 · Zbl 0208.20101
[4] de Bruijn, N.G., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indag. math., 34, 5, 381-392, (1972) · Zbl 0253.68007
[5] de Bruijn, N.G., Some extensions of automath: the AUT-4 family, (Jan. 1974), Internal Automath memo M10
[6] de Bruijn, N.G., A survey of the project automath, () · Zbl 0648.68099
[7] Cardelli, L., A polymorphic λ-calculus with type: type, (1986), Private communication
[8] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, (May 1985), Private communication
[9] Church, A., A set of postulates for the foundation of logic, Ann. math., (1932) · JFM 58.0070.02
[10] Church, A., A formulation of the simple theory of types, J. symbolic logic, 5, 1, 56-68, (1940) · JFM 66.1192.06
[11] Church, A., ()
[12] Constable, R.L., ()
[13] Constable, R.L.; Bates, J.L., (), TR 83-551
[14] Constable, R.L.; Mendler, N.P., Recursive definitions in type theory, () · Zbl 0579.68019
[15] Coquand, Th., Une théorie des constructions, ()
[16] Coquand, Th., An analysis of Girard’s paradox, ()
[17] Coquand, Th.; Huet, G., A theory of constructions, (), preliminary version
[18] Coquand, Th.; Huet, G., Constructions: A higher order proof system of mechanizing mathematics, () · Zbl 0581.03007
[19] Coquand, Th.; Huet, G., (), in press
[20] Curry, H.B.; Feys, R., ()
[21] Van Daalen, D., The language theory of automath, () · Zbl 0422.68045
[22] Fairbairn, J., Design and implementation of a simple typed language based on the lambda-calculus, (May 1985), University of Cambridge Computer Lab. Tech. Report 75
[23] Girard, J.Y., Une extension de l’interprétation de Gödel à l’analyse, et son application à l’émination des coupures dans l’analyse et la théorie des types, (), 63-92
[24] Girard, J.Y., Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieure, ()
[25] Gordon, M.J.; Milner, A.J.; Wadsworth, C.P., Edinburgh LCF, () · Zbl 0421.68039
[26] Howard, W.A., (), (1969), unpublished manuscript; reprinted in
[27] Huet, G., A unification algorithm for typed lambda calculus, Theoret. comput. sci., 1.1, 27-57, (1975) · Zbl 0337.68027
[28] Jutting, L.S., ()
[29] van Benthem Jutting, L.S., The language theory of λ∝ a typed λ-calculus where terms are types, (1984), unpublished manuscript
[30] Kleene, S.C., ()
[31] Lambek, J.; Scott, P.J., Aspects of higher order categorical logic, Contemp. math., 30, 145-174, (1984) · Zbl 0549.03058
[32] Martin-Löf, P., (), Report 71-3
[33] Martin-Löf, P., About models for intuitionistic type theories and the notion of definitional equality, () · Zbl 0334.02017
[34] Martin-Löf, P., An intuitionistic theory of types: predicative part, (), 73-118
[35] Martin-Löf, P., Constructive mathematics and computer programming, (), 153-175 · Zbl 0552.03040
[36] Martin-Löf, P., Intuitionistic type theory, Studies in proof theory, lecture notes, bibliopolis, Naples, (1984)
[37] McCraken, N., An investigation of a programming language with a polymorphic type structure, ()
[38] Nederpelt, R.P., Strong normalization in a typed λ calculus with λ structured types, () · Zbl 0438.68053
[39] Nederpelt, R.P., An approach to theorem proving on the basis of a typed λ-calculus, () · Zbl 0438.68053
[40] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[41] Reynolds, J.C., Polymorphism is not set-theoretic, () · Zbl 0554.03012
[42] Scott, D., Constructive validity, () · Zbl 0206.28402
[43] Seldin, J.P., Progress report on generalized functionality, Ann. math. logic., 17, (1979) · Zbl 0442.03014
[44] Stenlund, S., ()
[45] Tait, W., A realizability interpretation of the theory of species, () · Zbl 0328.02014
[46] Takeuti, G., On a generalized logic calculus, Japan J. math., 23, (1953) · Zbl 0053.20202
[47] Takeuti, G., Proof theory, Stud. logic, 81, (1975) · Zbl 0354.02027
[48] Whitehead, A.N.; Russell, B., ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.