Computer Science Department
School of Computer Science, Carnegie Mellon University
An Interpretation of Standard ML in Type Theory
Robert Harper, Christopher Stone
Also appears as Fox Project Technical Report CMU-CS-FOX-97-01.
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.