Changes between Version 5 and Version 6 of WikiStart


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

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v5 v6  
    2121* Uses the 'Case' meta-tactic to add structure.
    2222
     23== Installation ==
    2324
    24 == Simple ==
     25 * You will need a working version of [http://coq.inria.fr Coq]. The proofs are known to work with Coq 8.4.
     26
     27 * We use [http://darcs.net/ darcs] for version control.
     28{{{
     29$ darcs get http://code.ouroborus.net/iron/iron-head/
     30}}}
     31
     32
     33== [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/Simple/ Simple] ==
    2534Simply Typed Lambda Calculus (STLC).
    2635
    2736"Simple" here refers to the lack of polymorphism.
    2837
    29 == SimplePCF ==
     38==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimplePCF/ SimplePCF] ==
    3039STLC with booleans, naturals and fixpoint.
    3140
    32 == !SimpleRef ==
     41==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimpleRef/ SimpleRef] ==
    3342STLC with mutable references.
    3443
    3544The typing judgement includes a store typing.
    3645
    37 == !SimpleData ==
     46==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimpleData/ SimpleData] ==
    3847STLC with algebraic data and case expressions.
    3948
    4049The 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.
    4150
    42 == SystemF ==
     51==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF/ SystemF] ==
    4352Compared to STLC, the proof for SystemF needs more lifting lemmas so it can deal with deBruijn indices at the type level.
    4453
    45 == SystemF2 ==
     54==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2/ SystemF2] ==
    4655Very similar to SystemF, but with higher kinds.
    4756
    48 == SystemF2Data ==
     57==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2Data SystemF2Data] ==
    4958SystemF2 with algebraic data and case expressions.
    5059Requires 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.
    5160
    52 == SystemF2Store ==
     61==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2Store/ SystemF2Store] ==
    5362SystemF2 with algebraic data, case expressions and a mutable store.
    5463All data is allocated into the store and can be updated with primitive
    5564polymorphic update operators.
    5665
    57 == SystemF2Effect ==
     66==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2Effect/ SystemF2Effect] ==
    5867 * Still under development.
    5968