The calculus of constructions (Q1108266)

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).