The Coq mailing list

[Ben Lippmeier <benl AT ouroborus.net>]

Iron Lambda (http://iron.ouroborus.net/) is a collection of ​Coq 
formalisations for functional languages of increasing complexity. It fills 
part of the gap between the end of the​ Software Foundations course and what 
appears in current research papers.

The collection has at least Progress and Preservation theorems for the 
following languages. All but the last also have a big step evaluation 
semantics and round-trip lemmas between the small and big-step evaluation. 
All proofs just use straight deBruijn indices for binders.

* Simple        (STLC)
* SimplePCF     (... with booleans, naturals and fixpoint)
* SimpleRef     (... with mutable references)
* SimpleData    (... with algebraic data and case-expressions)

* SystemF   
* SystemF2      (Like SystemF but with higher kinds)
* SystemF2Data  (... with algebraic data and case-expressions)
* SystemF2Store (... with mutable algebraic data and case-expressions)

Cheers,
Ben.