Risorsa Analitica di Monografia

The Calculus of Constructions is a higher–order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn [2,3], Girard [12], Martin–L+Âf[14] and Scott [18]. The calculus and its syntactic theory were presented in Coquand's thesis [7], and an implementation by the author was used to mechanically verify a substantial number of proofs demonstrating the power of expression of the formalism [9]. The Calculus of Constructions is proposed as a foundation for the design of programming environments where programs are developed consistently with formal specifications. The current paper shows how to define inductive concepts in the calculus