[POPLmark] List machine 2.0

[Andrew W. Appel]

The List Machine Benchmark (Appel and Leroy 2006) was introduced as a
vehicle for comparing techniques for machine-checked proofs about Typed
Assembly Languages.  At that time we compared syntactic
(progress/preservation) proofs in Coq vs. Twelf.

Rob Dockins and I are happy to announce

List Machine 2.0
http://www.cs.princeton.edu/~appel/listmachine/2.0/

in which we present a fully worked demonstration in Coq, comparing
syntactic (progress/preservation) and semantic (very modal model) proofs
of type soundness for a simple Typed Assembly Language.

At the moment, although the Coq development is fairly clean and well
organized, there is not much documentation.  References [1] and [4] on
the web site may be helpful, in a general way.

-- Andrew Appel