[POPLmark] List machine 2.0

[Adam Chlipala]

Andrew W. Appel wrote:
> 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.
>   

I've posted another semantic solution in Coq at:
    http://adam.chlipala.net/poplmark/listmach_ltamer.tgz

My solution is 454 lines (not using anything from the benchmark 
distribution besides those symbols exported from the [simple_tc_safety] 
module), including a good amount of type definition/theorem statement 
boilerplate copied from the definition of the [SIMPLE_TC_SAFETY] 
signature.  Every theorem is proved with a single tactic.  This leaves 
complicated compound tactics as fair game, but rules out brittle proofs 
that refer to dynamically generated names.

I define the meanings of types using the dead obvious logical relation.

One of the most tiresome parts of working with the formalization in 
[Machine] was that it forced me to think about step counts too much.  
I've found that co-inductive semantics hide all of that nitty-gritty 
nicely.  It would also be nice to remove the need to prove determinism 
of the step relation explicitly by making [step] a function.  Here I'm 
just trying to transfer what I've found to work well with higher-level 
languages, but I haven't seen any reason yet to doubt that the same 
approach won't transfer well to assembly language.