@device(postscript) @libraryfile(Mathematics10) @libraryfile(Accents) @style(fontfamily=timesroman,fontscale=11) @pagefooting(immediate, left "@c", center "@c", right "@c") @heading @heading(CMU-CS-96-136R) @center(@b(Chris Stone, Robert Harper)) @center(September 1996@foot) @center(FTP: CMU-CS-96-136R.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. Version 2 of this document supersedes Version 1 (which was distributed as CMU SCS Technical Report CMU-CS-96-136). This version corrects serveral erros; it also includes a simpler internal language, an improved presentation of the dynamic semantics, an account of equality polymorphism, and an example extension of the language to handle lazy data structures. @blankspace(2line) @begin(transparent,size=10) @b(Keywords:@ )@c @end(transparent) @blankspace(1line) @end(text) @flushright(@b[(86 pages)])