X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=684cefd20c2e23e8a2ff6017100462e015697272;hb=5e5f9111df82a2f84f2b560ab59392cf0e0906c0;hp=5184a4d124aea90b5d754c53e9cf4afb2429fa88;hpb=68b5af5ca8f1e7f98485b92692b3dcb1ae240d19;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 5184a4d12..684cefd20 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -16,14 +16,14 @@
- [lambdadelta home] + [\lambda\delta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
- [Spacer] + [Spacer]
-
+

@@ -31,93 +31,109 @@ - home + home news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - - foreword + foreword milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + + Open Symbolic Notation (OSN) - citations + citations visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)
- -
Contents of the Specification [spacer] +
Contents of the Specification [butterfly]
-
This specification comprises a collection of checked +
This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.
-
    +
    • - MLTT1. + MLTT1. Martin-Löf's Type Theory with one universe using λδ as theory of expressions.
    -
      +
      • - Functional. + Functional. The validation algorithm for λδ as implemented in Helena 0.8.
      - -
      Summary of the Specification [spacer] +
        +
      • + Examples. + Terms of λδ with special features. +
        • +
      +
      Summary of the Specification [butterfly]
      -
      Here is a numerical acount of the specification's contents +
      Here is a numerical account of the specification's contents and its timeline.
      -
      +
      @@ -142,58 +158,63 @@ - + - + - + - + - + - + - + - +
      sizes files141 characters6787377 nodes10070779
      propositions theorems 2 lemmas41 total63
      concepts declared60 defined113 total173
      -
        +
          +
        • + 2017 March 6. + The Examples component is moved from the Core directory. +
          • +
        +
        • 2012 February 24. The Applications directory is started.
        -
          +
          • 2011 December 20. The Functional component is started inside the specification of λδ version 2.
          -
            +
            • 2011 December 12. The MLTT1 component is started.
            - -
            Logical Structure of the Specification [spacer] +
            Logical Structure of the Specification [butterfly]
            -
            This table reports the specification's components and their planes. +
            This table reports the specification's components and their planes.
            -
            +
            @@ -205,17 +226,25 @@ - - - - + + + + - - - + + + + + + + + @@ -223,9 +252,8 @@
            functionalreduction and type machinertmrtm_step ( ? ⇨ ? )functionalreduction and type machinertmrtm_step ( ? ⇨ ? )
            +
            		relocationlift ( ↑[?,?] ? )relocationlift ( ↑[?,?] ? ) +
            +
            examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
            - -
            - [Spacer] +
            + [Spacer]

            @@ -250,6 +278,6 @@

            -
            Last update: Wed, 24 Dec 2014 22:58:52 +0100
            - +
            Last update: Sat, 01 Apr 2017 16:50:39 +0200
            +