Constructor subtyping: extended version

Abstract

Constructor subtyping is a form of subtyping in which an inductive type $\sigma$ is viewed as a subtype of another inductive type $\tau$ if $\tau$ has more elements than $\sigma$. Its (potential) uses include proof assistants and functional programming languages.

In this report, we introduce and study the properties of a simply typed $\lambda$-calculus which supports constructor subtyping. We show that the calculus is well-behaved and provides a suitable basis for formalizing natural semantics in proof-development systems.