A Type-Theoretic Interpretation of Standard ML

It has been nearly twenty years since Robin Milner introduced ML as the metalanguage of the LCF interactive theorem prover [5]. His elegant use of abstract types to ensure validity of machine-generated proofs, combined with his innovative and flexible polymorphic type discipline, and supported by his rigorous proof of soundness for the language, inspired a large body of research into the type structure of programming languages.1 As a design tool type theory gives substance to informal ideas such as "orthogonality" and "safety" and provides a framework for evaluating and comparing languages. As an implementation tool type theory provides a framework for structuring compilers and supports the use of efficient data representations even in the presence of polymorphism [28, 27].