Type checking with universes (Q1177937)

The calculus of constructions (CC) was introduced by \textit{T. Coquand} and \textit{G. Huet} [Lect. Notes Comput. Sci. 203, 151-184 (1985; Zbl 0581.03007)]as a comprehensive basis for the formalization of constructive mathematics. The generalized calculus of constructions (\(CC^ \omega\)) was introduced by \textit{T. Coquand} [An analysis of Girard's paradox, Proc. Symp. on Logic in Computer Science (1986)]by extending the basic CC with a full cumulative hierarchy of type universes (a universe being a type that is closed under the type-forming operations of the calculus: the formation of products and strong sums indexed by a type of that universe level).] The authors study the type checking and well-typedness problems for four variants of \(CC^ \omega\). The paper is organized in seven sections, the first being an introduction. \(CC^ \omega\) is presented in Section 2 and some of its important properties are recalled. An operational presentation of the calculus with the property that at ost one rule of inference applies to a term is given in Section 3. The significance of this presentation is that it provides a normal form for typing derivations that is exploited by the type synthesis algorithm. In Section 4 a schematic type synthesis algorithm is presented that given a valid context \(\Gamma\) and a term \(M\), yields schematic description of the set of possible types for \(M\) with respect to \(\Gamma\). It is also shown that the well-typedness and type checking problems for \(CC^ \omega\) are effectively solved. These two problems are also studied in Section 5 for the extension of \(CC^ \omega\) with an ``anonymous'' universe. In Section 6 the authors extend both the basic calculus and the calculus with anonymous universes to admit definitions in the form of \(\delta\)- reductions. This extension leads to a notion of universe polimorphism analogous to the type polymorphism of \(ML\). Related research is discussed in the final section. It is also mentioned that \textit{Z. Luo}, \textit{R. Pollak} and \textit{P. Taylor} [How to use lego: A preliminary user's manual, Technical Report LFCS-TN-27, Edinburg (1989)]\ have implemented the algorithms of this paper in the Lego proof checker.