X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=eda6bd9352ce0bdecbe4595961641d36a877a73d;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=8eacf793043ca51af839ac6d8e0b6e3b55c41090;hpb=ddd6cb6f4514d9ca97f857cafa218c170222f5aa;p=helm.git diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 8eacf7930..eda6bd935 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -19,202 +19,230 @@ [lambdadelta home] -
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
[Spacer]
-
+

- - - - - - - - - - - - - - - - - + - - -
+ home + news - documentation + + specification - implementation + +
(specifications - library - Helena)
- Foreword + +
- Milestones + + documentation - Version 2 + + implementation - Version 2 + +
(Background - Core - Applications)
- Notice + + foreword - Visibility + + milestones - Version 1 + + version 2 - Version 1 - + (background - core - applications)
-
- -
Computer-checked formal specifications [spacer] -
-
- λδ comes in several versions listed in the following table, - which includes the major milestones: -
-
- - - - - - - - - - - - - - - - - - - + - - - + + + + + + - - - -
versionnamedeveloped withstartedannouncedreleaseddismissed
2 - basic_2 + + version 2 - Matita 0.99.2 + + library April 2011July 2014Planned in 2014Not planned yet(static LDDL directory)
1 - basic_1 + + citations - Coq 7.3.1 + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + helena + +
May 2004January 2006November 2006May 2008
- -
Tools [spacer] +
Tools [spacer]
- -
+
[Crux logo] λδ Digital Library (LDDL)
-
+
The λδ Digital Library is part of HELM - and contains resources expressed in λδ. + and contains resources expressed in the systems of the λδ family.
-
    +
    • - 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 the systems of the λδ family, 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. + meant for testing both their stable and unstable features.
        -
        +
        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.3 (2015-12). + Supports exportation to λProlog + (two formats for ELPI, + and two formats for Teyjus). + Employs optimized conditional compilation through + camlp5 code preprocessor (pa_macro) + to reduce a performance loss, which is expected to disappear + by employing a different code preprocessor. + Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2: + +3% with optimized compilation, +5% without optimized compilation. + [Svn revision: 13108] (archived source code). +
              +
            • + 2015-06. + The corrected specification of Landau's "Grundlagen der Analysis" + is successfully validated in a λProlog implementation of λδ version 3. +
              • +
            +
          -
            +
            • - Version 0.8.1 (2010-11). - Exploits a subset of "complete_rg" λδ as the intermediate language. + 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 (J3a). + [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 CC 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). + 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). + Documentation (R2a). [Svn revision: 10304] (archived source code).
                • @@ -222,22 +250,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]
              @@ -263,6 +291,6 @@

              -
              Last update: Tue, 05 Aug 2014 23:07:40 +0200
              - +
              Last update: Fri, 01 Apr 2016 23:30:52 +0200
              +