Computer Science Department
School of Computer Science, Carnegie Mellon University


A Formulation of Dependent ML
with Explicit Equality Proofs

Daniel R. Licata, Robert Harper

December 2005

Keywords: Type systems, dependent types, ML, phase distinction, explicit 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 Dependent ML, Epigram, Cayenne, ATS, Ωmega, and RSP1.

74 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by