Changes between Version 11 and Version 12 of WikiStart


Ignore:
Timestamp:
Dec 27, 2012, 2:56:31 PM (9 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v11 v12  
    11= Iron Lambda =
    22
    3 Iron Lambda is a collection of Coq formalisations for functional languages
    4 of various complexities. The aim of the project is to get the proofs done
    5 and not worry too much about using the coolest new approaches.
     3Iron Lambda is a collection of Coq formalisations for functional languages of increasing complexity. The aim of the project is to get the proofs done and not worry too much about using the coolest new approaches.
    64
    75All proofs use straight deBruijn indices for binders, which are fairly usable once you understand what lifting lemmas are required. They use a "semi-[http://adam.chlipala.net/cpdt/ Chilpala]" approach to mechanisation -- most lemmas are added to the global hint and rewrite databases, but if the proof script of a particular lemma was already of a sane length, then we haven't invested time writing tricky LTac code to make it smaller.