A Syntactic Account of Singleton Types Via Hereditary Substitution

The authors give a syntactic proof of decidability and consistency of equivalence for the singleton type calculus, which lies at the foundation of modern module systems such as that of ML. Unlike existing proofs, which work by constructing a model, their syntactic proof makes few demands on the underlying proof theory and mathematical foundation. Consequently, it can be - and has been - entirely formulated in the Twelf meta-logic, and provides an important piece of a Twelf-formalized type-safety proof for Standard ML. The proof works by translation of the singleton type calculus into a canonical presentation, adapted from work on logical frameworks, in which equivalent terms are written identically.