| An Effective Stable Domain Model of the Calculus of Construction Extended by Strong Sums and Recursive Definitions (2008) | |||||||||||||
Abstract | |||||||||||||
| We present a purely domain-theoretic model of Coquand and Huet’s Calculus of Construction [3], which is one of the most powerful type systems proposed in the literature. The well-formed expressions of its language are divided into three levels: Terms, Types, and Orders. Terms are the elements of Types, while the elements of Orders are called Operators. There is a special Order constant Type denoting the collection of all Types. Orders are closed under both, the dependent product and the dependent sum of Order families indexed over an Order or a Type. In the same way, Types are closed under the dependent product as well as the dependent sum of Type families indexed over an Order or a Type. In addition, we allow recursive definitions at all three levels. As a subsystem the calculus contains Girard-Reynold’s polymorphic λ-calculus [4, 5, 7]. Building upon ideas of Girard [6], Coquand et al. [2] presented a model of this subcalculus in which Types are interpreted as dI-domains. It is well known that each such domain can be represented as the state set of a | |||||||||||||
Details der Publikation | |||||||||||||
| |||||||||||||