Changes between Version 12 and Version 13 of WikiStart


Ignore:
Timestamp:
Dec 27, 2012, 3:06:26 PM (9 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v12 v13  
    11= Iron Lambda =
    22
    3 Iron 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.
     3Iron Lambda is a collection of [http://coq.inria.fr Coq] formalisations for functional languages of increasing complexity. It fills part of the gap between the end of the [http://www.cis.upenn.edu/~bcpierce/sf/ Software Foundations] course and what appears in current research papers. If you are new to Coq then you would be better off starting with Software Foundations rather than this work.
    44
    5 All 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.
     5As the focus of Iron Lambda is more on programming language semantics than the coolest new proving techniques, we just use straight deBruijn indices for binders. Using deBruijn indices does require that we prove some lemmas about lifting and substitution, but they are very similar between languages, so the initial effort can be re-used. For more details see the blog post [http://disciple-devel.blogspot.com.au/2011/08/how-i-learned-to-stop-worrying-and-love.html How I learned to stop worrying and love deBruijn indices.]
     6
     7The proofs 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.
    68
    79Style guidelines: