[TYPES] mechanized metatheory of standard ml alpha release

[Robert Harper]

Motivated by the current interest in many aspects of mechanized  
metatheory for programming languages, we are releasing an "alpha"  
version of our mechanization of the metatheory of standard ml, which  
is available from our respective publications pages.  The tarball that  
you will find there contains the formalization and verification of  
Standard ML by elaboration into an internal language, as described in  
our POPL paper with Daniel Lee.  It should be understood that this is  
an alpha release that certainly needs polishing for presentation and  
clarity, and may be revised before we go to a full publication.   
Additionally, it is also possible that it may contain errors, not that  
compromise safety, but that may depart from the intended semantics.   
We are currently validating the mechanization to rule out such  
mistakes.  We do, however, deliberately exclude some obsolete or  
deprecated features of Standard ML (notably equality types).

Thanks for your interest!
Karl Crary
Bob Harper