A syntactic account of singleton types via hereditary substitution

摘要

We 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, our 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.