Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
Feb 18, 2014
Feb 18, 2014
Feb 18, 2014
il
Feb 18, 2014
Feb 18, 2014
Feb 18, 2014
Feb 18, 2014

The-Mechanization-of-Standard-ML

A fully formalized elaborative semantics for Standard ML based on the interpretation given by Harper and Stone (see the Milner Festschrifft). Contains a formal definition of the statics and dynamics of the internal type theory of Standard ML, and a formalized elaboration from the Standard ML external language into the internal language. Also contains a machine-checked proof of type safety of the internal language, and a machine-checked proof that well-elaborated programs are type correct. Therefore, well-elaborated Standard ML programs cannot incur a run-time error arising from a misapplication of a primitve to a value.

This is the first, and until now, only fully formalized, machine-checked definition of a full-scale usable programming language. The mechanization was carried out by Karl Crary and Robert Harper using "pair programming", meeting once per week for 2-3 hours over the course of a semester. It was not difficult to pick up the work from week to week, and there were no great obstacles to the mechanization effort. The prior work of Mark Lillibridge, Chris Stone, Daniel Lee, and the authors prepared the ground. The project confirms the experience that one cannot expect to carry out a verification of an artifact "thrown over the wall", but that it is entirely practical to do so if the development is carried out with verification in mind. This is a well-known fact about programs in general; this work confirms the experience for programming languages themselves.

About

The Mechanization of Standard ML

Resources

Releases

No releases published

Packages

No packages published