A Formulation of Dependent ML with Explicit Equality Proofs
Daniel R. Licata, Robert W. Harper · 2018
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.