Changes between Version 2 and Version 3 of WikiStart


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

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v2 v3  
    11= Iron Lambda =
    22
     3Iron Lambda is a collection of Coq formalisations for functional languages
     4of various complexities. The aim of the project was to get the proofs done
     5and not worry much about using the coolest new approaches.
     6
     7All proofs use straight deBruijn indices for binders, which aren't too bad
     8once you understand what lifting lemmas are required. They use a
     9"semi-Chilpala" approach to mechanisation -- most lemmas are added to the
     10global hint and rewrite databases, but if the proof script of a particular
     11lemma was already of a sane length, then we haven't invested time writing
     12tricky LTac code to make it smaller.
     13
     14Style guidelines:
     15
     16* Verbose comments explaining what the main definitions and theorems
     17  are for. The scripts should be digestable by intermediate Coq users.
     18 
     19* No unicode or infix operators for judgement forms.
     20  When *I* use them in *my* proofs they make perfect sense, but when you
     21  use them in yours they're completely unreadable.
     22
     23* 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...
     25
     26* Uses the 'Case' meta-tactic to add structure.
     27
     28
     29== Simple ==
     30Simply Typed Lambda Calculus (STLC).
     31
     32"Simple" here refers to the lack of polymorphism.
     33
     34== SimplePCF ==
     35STLC with booleans, naturals and fixpoint.
     36
     37== !SimpleRef ==
     38STLC with mutable references.
     39
     40The typing judgement includes a store typing.
     41
     42== !SimpleData ==
     43STLC with algebraic data and case expressions.
     44
     45The definition of expressions uses indirect mutual recursion. Expressions contain a list of case-alternatives, and alternatives contain expressions, but the definition of the list type is not part of the same recursive group. The proof requires that we define our own induction scheme for expressions.
     46
     47== SystemF ==
     48Compared to STLC, the proof for SystemF needs more lifting lemmas so it can deal with deBruijn indices at the type level.
     49
     50== SystemF2 ==
     51Very similar to SystemF, but with higher kinds.
     52
     53== SystemF2Data ==
     54SystemF2 with algebraic data and case expressions.
     55Requires that we define simultaneous substitutions, which are used when subsituting expressions bound by pattern variables into the body of an alternative. The language allows data constructors to be applied to general expressions rather than just values, which requires more work when defining evaluation contexts.
     56
     57== SystemF2Store ==
     58SystemF2 with algebraic data, case expressions and a mutable store.
     59All data is allocated into the store and can be updated with primitive
     60polymorphic update operators.
     61
     62== SystemF2Effect ==
     63 * Still under development.
     64
     65SystemF2 with a region and effect system.
     66