A Formulation of Dependent ML with Explicit Equality Proofs

We study a calculus that supports dependent programming in the style of Xi and Pfenning’s Dependent ML. Xi and Pfenning’s language determines equality of static data using a built-in decision procedure; ours permits explicit, programmer-written proofs of equality. In this report, we define our calculus’ semantics and prove type safety and decidability of type checking; we have mechanized much of these proofs using the Twelf proof assistant. Additionally, we illustrate programming in our calculus through a series of examples. Finally, we present a detailed comparison with other dependently typed languages, including DependentML, Epigram, Cayenne, ATS, ­Ωmega, and RSP1.