The calculus of constructions
type: Item
instance of: scholarly article
title: The calculus of constructions
zbMATH Open document ID: 0654.03045
DOI: 10.1016/0890-5401(88)90005-3
author: Thierry Coquand
author: Gérard Huet
published in: Information and Computation
publication date: 1988-01-01T00:00:00Z
review text: 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 \textit{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 \textit{Th. Ehrhard}'s thesis (Paris VII, 1988) and in \textit{Th. Streicher}'s thesis (Passau, 1988).
reviewed by: Thierry Coquand
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 4066877
zbMATH Keywords: impredicative extension of Martin-Löf type theory
zbMATH Keywords: functional system
zbMATH Keywords: Automath
zbMATH Keywords: type system for functional programming
zbMATH Keywords: mechanized mathematics
zbMATH Keywords: realizability interpretation
zbMATH Keywords: untyped \(\lambda \) -calculus
Wikidata QID: Q56385237
describes a project that uses: Automath
MaRDI profile type: Publication
full work available at URL: 0890-5401(88)90005-3
OpenAlex ID: W1986402635
cites work: The lambda calculus, its syntax and semantics
cites work: Semantics for classical AUTOMATH and related systems
cites work: Q5610115
cites work: Q5667469
cites work: Q3793765
cites work: Q3702502
cites work: Q3703866
cites work: Q3030827
cites work: Q5565113
cites work: Q3856127
cites work: Q5625124
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q3922646
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Q5812175
cites work: Q3342573
cites work: Q4099614
cites work: Q4099613
cites work: Constructive mathematics and computer programming
cites work: Q3688389
cites work: Q3880323
cites work: Q4068054
cites work: Q3216629
cites work: Q5606586
cites work: Progress report on generalized functionality
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Q4093416
cites work: Q5822068
cites work: Proof theory
description: scientific article; zbMATH DE number 4066877