A Higher-order Calculus and Theory Abstraction

Zhaohui Luo

Abstract: We present a higher-order calculus Sigma CC_\subset that can be seen as an extension of Coquand-Huet's calculus of constructions (CC) [CH88] by adding strong sum types and including propositions as types. Strong sum types in Sigma CC_\subset provides a useful module mechanism so that abstract structures can be naturally expressed and theories can be thoroughly abstracted, leading to a comprehensive structuring of mathematical texts in proof development. Including propositions as types solves the technical difficulty that adding (type-indexed) strong sums to the proposition level of CC results in inconsistency [Coq86a].

We give an omega-Set model construction of Sigma CC_\subset using the idea developed by E. Moggi [Mog85][LM88], which entails the consistency of the calculus and establishes the theoretical soundness of using strong sum types to express abstract structures and structurally develop theories in the calculus.

Extending Sigma CC_\subset with an infinite type hierarchy results in the system Sigma CC \stackrel{\infty} {\subset}, which is more expressive and more flexible for structuring theories. Sigma CC \stackrel{\infty}{\subset} is still strongly normalizing and henceforth consistent, although its type levels are weakly impredicative.

LFCS report ECS-LFCS-88-57

Previous | Index | Next