×

Concepts mathématiques et informatiques formalisés dans le calcul des constructions. (French) Zbl 0627.03045

Logic colloq. ’85, Proc. Colloq., Orsay/France 1985, Stud. Logic Found. Math. 122, 123-146 (1987).
[For the entire collection see Zbl 0611.00002.]
This paper presents an early version of the “calculus of construction”. This calculus is an attempt to give a synthesis of P. Martin-Löf’s intuitionistic theory of types, and of J. Y. Girard’s \(F\omega\) functional system (developed as a generalisation the Dialectica interpretation to higher-order logic). The main aim of the authors is the mechanisation of such a system, and for this purpose they use the suggestive notation of Automath, invented by N. De Brujin. The calculus may then be seen naturally as a formalisation of higher-order natural deduction, well suited for an implementation. Some simple examples are given: proofs in higher-order logic and how to translate second-order \(\lambda\)-calculus.
This paper does not mention the semantical issue, and it must be noted that there exist now “natural” models of this system, generalising J. Y. Girard’s model of polymorphism [see the papers of Hyland-Pitts and Lamarche in “Categories in Computer Science and Logic”, Contemporary Math., Amer. Math. Soc., Providence RI (to appear)].

MSC:

03F99 Proof theory and constructive mathematics
68Q65 Abstract data types; algebraic specification

Citations:

Zbl 0611.00002

Software:

Automath