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, Omega, and RSP1.