## 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