CMU-CS-97-147Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-97-147
Robert Harper, Christopher Stone June 1997
Also appears as Fox Project Technical Report CMU-CS-FOX-97-01.
Keywords: Standard ML, type theory, semantics, programming language
design, compilation, translation, elaboration, static semantics, dynamic
semantics
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. 78 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |