Coquand, Thierry; Huet, Gérard 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)]. Cited in 6 Documents MSC: 03F99 Proof theory and constructive mathematics 68Q65 Abstract data types; algebraic specification Keywords:Curry-Howard isomorphism; interactive proof system; intuitionistic type theory; calculus of construction; Automath; formalisation of higher-order natural deduction Citations:Zbl 0611.00002 Software:Automath PDFBibTeX XML