A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML

This paper describes a syntactic translation for a substantial fragment of the core Standard ML language into a typed lambda-calculus with recursive types and imperative features in the form of reference types. The translation compiles SML's use of declarations and pattern matching into lambda-terms, and transforms the use of environments in the operational semantics into a simpler relation of evaluation to canonical form. The translation is shown to be "fully abstract", in the sense that it both preserves and reflects observational equivalence (also commonly called contextual equivalence). A co-inductively defined notion of applicative bisimilarity for lambda calculi with state is developed to establish this result.