@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading<A Type-Theoretic Account of Standard ML 1996
(Version 1)>
@heading(CMU-CS-96-136)
@center(@b(Chris Stone, Robert Harper))
@center(May 1996@foot<Also appears as CMU-CS-FOX-96-02>)
@center(FTP: CMU-CS-96-136.ps)
@blankspace(1)
@begin(text)

A type-theoretic definition of a variant of the Standard ML (Revised
1996) programming language is given.  The definition consists of a
syntax-directed translation of SML96 programs into a typed
intermediate language.  The intermediate language is an
explicitly-typed @g(l)-calculus with product, sum, recursive, and
module types.  The translation performs type reconstruction, handles
identifier scope resolution, enforces static well-formedness
conditions, and expands high-level constructs (such as pattern
matching and signature matching) into uses of the more rudimentary
mechanisms of the intermediate language.  

This document presents work in progress and is being distributed for
the purpose of obtaining feedback.  As such, the translation does not
completely match the definition of SML96, which is itself still
undergoing change.


@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Standard ML, type theory, semantics, programming language
design, compilation, translation, elaboration, static semantics, dynamic
semantics>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(89 pages)])