X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e1e8448af4e74e60b2ba048f7cfdc6a484f2b5bf;hb=6ce2552192c2727eb5f7d17f52b949549e1e6ad1;hp=5cdf1b2ff7b8e27fda97dba3f5a7c07197204b18;hpb=b665b25cc0b62aa5bd7e90224fe7a28d15e122f2;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5cdf1b2ff..e1e8448af 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,30 +84,42 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - helena -
- - -
Summary of the Specification [spacer] + +
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
-
+
@@ -122,20 +144,20 @@ - + - + - + - + - + @@ -149,53 +171,51 @@
sizes files358360 characters431837437272 nodes18601621935835
propositions theorems 130 lemmas12861303 total14161433
concepts
- -
Stage "B"
-
    +
    Stage "B"
    +
    • Ongoing. Context-sensitive subject equivalence for native type assignment.
    - -
    Stage "A": "Extending the Applicability Condition"
    -
      +
      Stage "A": "Extending the Applicability Condition"
      +
      • 2014 October 28. λδ version 2A is released.
      -
        +
        • 2014 September 9. Iterated static type assignment defined (more elegantly) as a primitive notion.
        -
          +
          • 2014 June 18. Preservation of stratified native validity for context-sensitive computation on terms.
          -
            +
            • 2014 June 9. Strong qrst-normalization for simply typed terms.
            -
              +
              • 2014 April 16. Lazy equivalence on local environments - addded as q-step to rst-computation on closures + added as q-step to rst-computation on closures (anniversary milestone).
              -
                +
                • 2014 January 20. Parametrized slicing of local environments @@ -203,26 +223,26 @@ (one from basic_1, the other used in basic_2 till now).
                -
                  +
                  • 2013 August 7. Passive support for global environments.
                  -
                    +
                    • 2013 July 27. Reaxiomatized β-reductum as in rt-reduction.
                    -
                      +
                      • 2013 July 20. Context-sensitive strong rt-normalization for simply typed terms.
                      -
                        +
                        • 2013 April 16. Reaxiomatized substitution and reduction @@ -230,26 +250,26 @@ (anniversary milestone).
                        -
                          +
                          • 2013 March 16. Mutual recursive preservation of stratified native validity for rst-computation on closures.
                          -
                            +
                            • 2012 October 16. Confluence for context-free parallel reduction on closures.
                            -
                              +
                              • 2012 July 26. Term binders polarized to control ζ-reduction (not released).
                              -
                                +
                                • 2012 April 16. Context-sensitive subject equivalence @@ -257,43 +277,42 @@ (anniversary milestone).
                                -
                                  +
                                  • 2012 March 15. Context-sensitive strong normalization for simply typed terms.
                                  -
                                    +
                                    • 2012 January 27. Support for abstract candidates of reducibility.
                                    -
                                      +
                                      • 2011 September 21. Confluence for context-sensitive parallel reduction on terms.
                                      -
                                        +
                                        • 2011 September 6. Confluence for context-free parallel reduction on terms.
                                        -
                                          +
                                          • 2011 April 17. Specification starts.
                                          - -
                                          Logical Structure of the Specification [spacer] +
                                          Logical Structure of the Specification [spacer]
                                          -
                                          This table reports the specification's components and their planes. +
                                          This table reports the specification's components and their planes.
                                          -
                                          +
                                          @@ -1000,7 +1019,7 @@ - + @@ -1140,7 +1159,7 @@ - +

                                          		contxt-sensitive multiple rt-substitutioncontext-sensitive multiple rt-substitution cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) cpys_lift cpys_cpys
                                          		contxt-sensitive ordinary rt-substitutioncontext-sensitive ordinary rt-substitution cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_nlift cpy_cpy @@ -1339,8 +1358,7 @@
                                          - -
                                          +
                                          [Spacer]
                                          @@ -1366,6 +1384,6 @@

                                          -
                                          Last update: Sat, 01 Nov 2014 17:50:22 +0100
                                          - +
                                          Last update: Wed, 02 Sep 2015 17:59:07 +0200
                                          +