Mechanizing the Metatheory of Standard ML

Our long-term goal is to have a complete mechanized definition and type safety proof for Standard ML. For the purposes of mechanization, we use the Twelf system, which is an implementation of the LF logical framework. For a number of reasons, we suspect it is untenable verify the metatheory of a formalism based on The Definition of Standard ML. Consequently, we have formalized a new interpretation of Standard ML in the style of Harper and Stone, with mechanization in mind. In a Harper-Stone style semantics, Standard ML is viewed as an external source language whose objects are given meaning via an elaboration into an explicitly typed internal language with a well-defined static and dynamic semantics. Currently, we have a complete definition and type safety proof for the internal language. Current work is on the definition of an elaborator from Standard ML to the internal language, as well as a proof that elaboration produces terms that are well-formed in the internal language.

This project is work by Daniel K. Lee, Karl Crary, and Robert Harper. Although this is a new formalism, we owe much to what was learned in an earlier attempt to mechanize the Harper-Stone interpretation of Standard ML that was chiefly done by Michael Ashley-Rollman with contributions from Susmit Sarkar. In addition, our internal language is heavily based on one presented in Derek Dreyer's PhD dissertation.

Towards a Mechanized Metatheory of Standard ML Technical Report
Twelf Source Code Release 07-14-2006.

In September 2006, we gave a presentation of our work at the 1st Workshop on Mechanizing Metatheory.

References

  • Derek Dreyer. Understanding and Evolving the ML Module System. Ph.D. Dissertation, CMU Technical Report CMU-CS-05-131, May 2005. PDF
  • Robert Harper and Chris Stone. A Type-Theoretic Interpretation of Standard ML. Milner Festschrifft. 2000. PDF.
  • Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

    • See the paper for a more exhaustive bibliography of related works!