X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=02abad18e413385580669717446bfa725204fadc;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=e503c0e3dd779eccbe397bf33e58880c7798471a;hpb=636db4e12452d2ebce318b36cf5c41d30e4d9c29;p=helm.git diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index e503c0e3d..02abad18e 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -16,14 +16,14 @@
- [lambdadelta home] + [\lambda\delta home]
-
The Formal System λδ (\lambda\delta)
+
The Formal Systems of the λδ (\lambda\delta) Family
- [Spacer] + [Spacer]
-
+

@@ -31,177 +31,253 @@ - 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) - notice + citations - citations + visibility + + + version 1 + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)
- -
Tools [spacer] +
Tools [butterfly]
- -
- [Crux logo] λδ Digital Library (LDDL)
-
- The λδ Digital Library is part of HELM - and contains resources expressed in λδ. +
+ + [Open Symbolic Notation logo] + Open Symbolic Notation
+
+ Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal languages. + Additional information is available at OSN web site.
-
    -
  • - 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.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). - 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). + Documentation (R2a). [Svn revision: 10304] (archived source code).
            -
          • +
          • A Jed mode 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.
          +
          • +
        +
        + [\lambda\delta digital library logo] λδ Digital Library (LDDL)
        +
        + The λδ Digital Library is part of HELM + and contains resources expressed in the systems of the λδ family. +
        +
          +
        • + Contents: + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath).
        -
        - [Spacer] + + +
        + [Spacer]

        @@ -226,6 +302,6 @@

        -
        Last update: Mon, 20 Oct 2014 16:17:00 +0200
        - +
        Last update: Fri, 24 Nov 2017 21:00:00 +0100
        +