Changes between Version 3 and Version 4 of WikiStart


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

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v3 v4  
    22
    33Iron Lambda is a collection of Coq formalisations for functional languages
    4 of various complexities. The aim of the project was to get the proofs done
    5 and not worry much about using the coolest new approaches.
     4of various complexities. The aim of the project is to get the proofs done
     5and not worry too much about using the coolest new approaches.
    66
    7 All proofs use straight deBruijn indices for binders, which aren't too bad
    8 once you understand what lifting lemmas are required. They use a
    9 "semi-Chilpala" approach to mechanisation -- most lemmas are added to the
    10 global hint and rewrite databases, but if the proof script of a particular
    11 lemma was already of a sane length, then we haven't invested time writing
    12 tricky LTac code to make it smaller.
     7All proofs use straight deBruijn indices for binders, which are fairly usable once you understand what lifting lemmas are required. They use a "semi-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.
    138
    149Style guidelines:
     
    1813 
    1914* No unicode or infix operators for judgement forms.
    20   When *I* use them in *my* proofs they make perfect sense, but when you
     15  When ''I'' use them in ''my'' proofs they make perfect sense, but when you
    2116  use them in yours they're completely unreadable.
    2217
    2318* Heavy use of the 'burn' megatactic. This is in the same vein as Chilpala's
    24  'crush' tactic, but I couldn't work out what 'crush' was doing...
     19 'crush' tactic, but at the time I couldn't work out what 'crush' was doing...
    2520
    2621* Uses the 'Case' meta-tactic to add structure.