RE: mechanical proof checkers for type soundness?
Subject: RE: mechanical proof checkers for type soundness?
From: Eric Allen - Sun Microsystems - Burlington United States <Eric.Allen@Sun.COM>
Date: Fri, 17 Oct 2003 15:54:44 -0400 (EDT)
Reply-To: Eric Allen - Sun Microsystems - Burlington United States <Eric.Allen@Sun.COM>
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
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
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
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
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