Changes between Version 29 and Version 30 of WikiStart
- Timestamp:
- Nov 29, 2013, 9:43:21 PM (11 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
WikiStart
v29 v30 55 55 Click the headings to get to the proofs.[[br]] 56 56 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] == 58 58 Simply Typed Lambda Calculus (STLC). 59 59 60 60 "Simple" here refers to the lack of polymorphism. 61 61 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] == 63 63 STLC with booleans, naturals and fixpoint. 64 64 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] == 66 66 STLC with mutable references. 67 67 68 68 The typing judgement includes a store typing. 69 69 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] == 71 71 STLC with algebraic data and case expressions. 72 72 73 73 The 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. 74 74 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] == 76 76 Compared to STLC, the proof for SystemF needs more lifting lemmas so it can deal with deBruijn indices at the type level. 77 77 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] == 79 79 Very similar to SystemF, but with higher kinds. 80 80 81 == [http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SystemF2DataSystemF2Data] ==81 == [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Data/ SystemF2Data] == 82 82 SystemF2 with algebraic data and case expressions. 83 83 Requires 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. 84 84 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] == 86 86 SystemF2 with algebraic data, case expressions and a mutable store. 87 87 All data is allocated into the store and can be updated with primitive 88 88 polymorphic update operators. 89 89 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] == 91 91 SystemF2 with a region and effect system. Supports region extension and deallocation. 92
