[Prev][Next][Index][Thread]

RE: mechanical proof checkers for type soundness?

Thank's very much to everyone who responded to my message. I've gotten several 
requests for information on what I've found, so I thought it would be useful to 
send a summary to the whole list.

Most of the responses pointed me to Twelf. I also got a few messages suggesting 
Isabelle, but ultimately I decided to go with Twelf. Twelf works best when 
working over a Plotkin-style Structural Operational Semantics. Apparently, Twelf 
is often able to prove progress and preservation from SOS-style semantics 
automatically.

I managed to install Twelf on OS X yesterday, and I learned the basics of using 
it in a few hours. So far, I love it. In addition to the Twelf documentation, I 
found Andrew Appel's course notes quite helpful (they're available from the 
Twelf homepage).

If you are interested in installing Twelf on OS X, here are a few tips:

1. If you want to compile Twelf with SML/NJ, and you're using Fink to install 
open-source software on OS X (as I highly recommend), you will notice that 
SML/NJ isn't yet supported as a "stable package". Here's a workaround: first, 
make sure you have the latest version of Fink by running "sudo fink selfupdate". 
Then transfer the files /sw/fink/dists/unstable/main/finkinfo/smlnj* to 
directory /sw/fink/dists/local/main/finkinfo. After that, you should be able to 
run "sudo fink install smlnj" without a problem.

2. After you install SML/NJ, you can follow the instructions to install Twelf 
as-is, but read the entire installation instructions before starting, because 
there is one command ("make") that you have to issue differently for the latest  
ML compilers.

3. The Twelf instructions give you commands for your .emacs file so that you can 
use the Twelf plug-in for Emacs. In order for that plug-in to work with 
carbonized Emacs, you have to make sure that Emacs reads your execution path 
when it starts up (it won't be set correctly by default). You can do this by 
running the "set-environment" application in the emacs-docs directory (included 
with the carbonized Emacs download). That app creates an XML file 

  ~/.MacOSX/environment.plist
  
Apparently the OS reads that file on startup, and sets global state accessed by 
Emacs. If you reboot after running that app, Emacs should get all of your path 
info.

-- Eric