Changes between Version 29 and Version 30 of WikiStart


Ignore:
Timestamp:
Nov 29, 2013, 9:43:21 PM (8 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v29 v30  
    5555Click the headings to get to the proofs.[[br]]
    5656
    57 == [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/Simple/ Simple] ==
     57== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/Simple/ Simple] ==
    5858Simply Typed Lambda Calculus (STLC).
    5959
    6060"Simple" here refers to the lack of polymorphism.
    6161
    62 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimplePCF/ SimplePCF] ==
     62== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SimplePCF/ SimplePCF] ==
    6363STLC with booleans, naturals and fixpoint.
    6464
    65 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimpleRef/ SimpleRef] ==
     65== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SimpleRef/ SimpleRef] ==
    6666STLC with mutable references.
    6767
    6868The typing judgement includes a store typing.
    6969
    70 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimpleData/ SimpleData] ==
     70== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SimpleData/ SimpleData] ==
    7171STLC with algebraic data and case expressions.
    7272
    7373The 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.
    7474
    75 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF/ SystemF] ==
     75== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF/ SystemF] ==
    7676Compared to STLC, the proof for SystemF needs more lifting lemmas so it can deal with deBruijn indices at the type level.
    7777
    78 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2/ SystemF2] ==
     78== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2/ SystemF2] ==
    7979Very similar to SystemF, but with higher kinds.
    8080
    81 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2Data SystemF2Data] ==
     81== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Data/ SystemF2Data] ==
    8282SystemF2 with algebraic data and case expressions.
    8383Requires 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.
    8484
    85 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2Store/ SystemF2Store] ==
     85== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Store/ SystemF2Store] ==
    8686SystemF2 with algebraic data, case expressions and a mutable store.
    8787All data is allocated into the store and can be updated with primitive
    8888polymorphic update operators.
    8989
    90 ==  [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2Effect/ SystemF2Effect] ==
     90== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Effect/ SystemF2Effect] ==
    9191SystemF2 with a region and effect system. Supports region extension and deallocation.
    92