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.