| Constructor subtyping in the Calculus of Inductive Constructions (2000) | |||||||||||||||
Abstract | |||||||||||||||
| The Calculus of Inductive Constructions (CIC) is a powerful type system, featuring dependent types and inductive definitions, that forms the basis of proof-assistant systems such as Coq and Lego. We extend CIC with constructor subtyping, a basic form of subtyping in which an inductive type σ is viewed as a subtype of another inductive type τ if τ has more elements than σ. It is shown that the calculus is well-behaved and provides a suitable basis for formalizing natural semantics in proof-development systems. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||