X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=f0e1d32ffe2616bfbb3397061e2a04bae253f26f;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=cd9cbf8995e5a3d0ad25c247b68fbd3edfb4d63b;hpb=1f1eb9d91faf1e905d44b5f44943b2db8472cc74;p=helm.git diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index cd9cbf899..f0e1d32ff 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -45,9 +45,15 @@
- + +
+ + implementation + +
+ @@ -63,13 +69,17 @@ version 2 (background - core - applications) - + +
+ + library + (static LDDL directory) - notice + citations visibility @@ -80,101 +90,134 @@ version 1 - -
- - + (background - core) + (static HELM directory) + helena + +
+
- -
Tools [spacer] +
Tools [spacer]
- -
+
[Crux logo] λδ Digital Library (LDDL)
-
+
The λδ Digital Library is part of HELM and contains resources expressed in λδ.
-
    +
    • - Contents: + Contents: Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath).
    -
      + -
        + - -
        +
        [Helena logo] Helena
        -
        - Helena is a λδ processor, +
        + Helena is a processor for λδ, implemented in Caml as a part of the HELM software, meant for testing the stable features of the calculus as well as the unstable ones.
        -
        +
        The processor source code is available in the directory /trunk/helm/software/helena/ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next.
        -
          +
          • - Version 0.8.2. - In progress. -
            • + Version 0.8.2 (2015-02). + Uses λδ "Version 3" with layer variables as core language. + Supports exportation to Gallina + (the specification language of Coq), + and to Grafite + (the specification language of Matita). + The overall validation speed of the "Grundlagen der Analysis" + increases of 34% with respect to version 0.8.1. + Documentation (J4). + [Svn revision: 13035] (archived source code). +
              +
            • + The specification of Landau's "Grundlagen der Analysis" + for Coq 8: + grundlagen_2.v + (revised 2015-02). +
              • +
            • + The specification of Landau's "Grundlagen der Analysis" + for Matita 0.99.2: + grundlagen_2.tar.bz2 + (revised 2015-02). +
              • +
            • + The corrected specification of Landau's "Grundlagen der Analysis": + grundlagen_2.aut + (revised 2014-12). +
              • +
            • + 2015-02. + The translated specification of Landau's "Grundlagen der Analysis" + is successfully validated in λC by Coq 8.4.3. +
              • +
            • + 2014-12. + The corrected specification of Landau's "Grundlagen der Analysis" + is successfully validated in λδ "Version 3". +
              • +
            +
          -
            +
            • - Version 0.8.1 (2010-11). - Exploits a subset of "complete_rg" λδ as the intermediate language. + Version 0.8.1 (2010-11). + Uses a subset of λδ "Version 4" as intermediate language. Features importation from ".hln" files containing λδ textual syntax. The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. - [Svn revision: 11032] (archived source code) + [Svn revision: 11032] (archived source code). -
              • +
            -
              +
              • - Version 0.8.0 (2009-09). - Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion. + Version 0.8.0 (2009-09). + Supports λδ "Version 2" with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. Documentation (R4). @@ -185,22 +228,22 @@ for editing ".aut" files (containing Automath textual syntax): automath.sl - (revised 2008-07). + (revised 2008-07).
              • - 2009-09. + 2009-09. Jutting's specification of Landau's "Grundlagen der Analysis" enters λδ Digital Library.
              • - 2009-06. + 2009-06. Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion.
              - +
            -
            +
            [Spacer]
            @@ -226,6 +269,6 @@

            -
            Last update: Tue, 14 Oct 2014 00:04:55 +0200
            - +
            Last update: Sat, 21 Feb 2015 23:38:38 +0100
            +