We define an interpretation of Standard~ML into type theory. The
interpretation takes the form of a set of elaboration rules reminiscent of the
static semantics given in \textit{The Definition of Standard ML}. In
particular, the elaboration rules are given in a relational style, exploiting
indeterminacy to avoid over-commitment to specific implementation techniques.
Elaboration consists of identifier scope resolution, type checking and type
inference, expansion of derived forms, pattern compilation, overloading
resolution, equality compilation, and the coercive aspects of signature
matching.
The underlying type theory is an explicitly-typed $\lambda$-calculus with
product, sum, function, and recursive types, together with module types
derived from the translucent sum formalism of Harper and Lillibridge.
Programs of the type theory are given a type-passing dynamic semantics
compatible with constructs such as polymorphic equality that rely on type
analysis at run-time.
This document supercedes the previous CMU CS technical reports
CMU-CS-96-136 and CMU-CS-96-136R. The revision reflects our
experience in implementing the specified elaborator, and includes
several essential corrections and simplifications to the presentation.