X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=8d16e68904737e59463c82497f9bbc47a73f0f4d;hb=9fc816ac51a681fe122712931f8df19d804a4695;hp=79f013900e7b10c901c0a498e7589377a219d986;hpb=77c6a180035cd63f3edd4db54bd7e9b411f9e85e;p=helm.git diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html index 79f013900..8d16e6890 100644 --- a/helm/www/lambda_delta/implementation.html +++ b/helm/www/lambda_delta/implementation.html @@ -1,281 +1,327 @@ - + - - - lambda_delta home page - - - - - -
-
-[Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - + + +
- - - -
    -
  • Resources
    -
    • -
- 		-

Computer-checked formal -specifications [Butterfly]

- Resource -1 below provides for the statically generated natural language representation of -λδ meta-theory (faster rendering w.r.t. resource 2 below).
- Resource 2 below provides -for the dynamically generated natural -language representation of -λδ meta-theory (powered by the HELM -rendering engine).
-Remarkably, λδ was born and developed in the digital format of resource 3 below, which is not the -formal counterpart of some informal material previously written on -paper (as it happens for most currently digitalized Mathematics).
-
    -
  1. F. Guidi: lambda_delta -(revised 2011-09). Formal -specification for Matita 0.5 -(HTML pages generated -by the HELM -rendering engine)
    -Here are the most relevant theorems proved in the formal specification: - -
    2. -
  2. F. Guidi: lambda_delta -(revised 2011-09). Formal -specification for Matita 0.5 (HELM directory).
    -
    -
    3. -
  3. F. Guidi: lambda_delta_1 -(revised 2011-09). -Formal specification for Coq 7.3.1 -(source -proof scripts). BibTeX entry.
    -
    4. -
-

Tools [Butterfly]

- [Crux Logo] The λδ -Digital -Library -(LDDL) is part of HELM -and contains a set of -resources expressed in λδ.
-
    -
  • Contents: Landau's "Grundlagen der Analysis" (from -Jutting's specification in Automath).
    -
    • -
- - + + + lambda_delta home page + + + + + +

- [Helena Logo] Helena is a λδ -processor, -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 below.
-
    -
-
    -
  • Version 0.8.2. In -progress.
    -
    • -
-
    -
  • Version 0.8.1 (2010-11). -Exploits a subset of "complete_rg" λδ as the 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) -
      -
    • 2009-12. Helena -appears in F. Wiedijk's index + [Crux Logo] +

      The Formal System λδ (lambda_delta)
      +

      +

      Towards the unification of terms, types, environments and + contexts

      + [Separator]
      + + + + + - - -
      + + + +
        +
      • Resources
        +
        • +
      +       		+

      Computer-checked formal + specifications [Butterfly]

      + Resource + 1 below provides for the statically generated natural language + representation of + λδ meta-theory (faster rendering w.r.t. resource 2 below).
      + Resource 2 below + provides + for the dynamically generated natural + language representation of + λδ meta-theory (powered by the HELM + rendering engine).
      + Remarkably, λδ was born and developed in the digital + format of resource 3 + below, which is not the + formal counterpart of some informal material previously + written on + paper (as it happens for most currently digitalized + Mathematics).
      +
        +
      1. F. Guidi: lambda_delta + (revised 2011-09). + Formal + specification for Matita 0.5 + (HTML pages generated + by the HELM + rendering engine)
        + Here are the most relevant theorems proved in the + formal specification: + +
        2. +
      2. F. Guidi: lambda_delta + (revised 2011-09). + Formal + specification for Matita 0.5 (HELM directory).
        +
        +
        3. +
      3. F. Guidi: lambda_delta_1 + (revised 2011-09). +Formal + specification for Coq + 7.3.1 + (source + proof scripts). BibTeX entry.
        +
        4. +
      +

      Tools [Butterfly]

      + [Crux Logo] The λδ + Digital + Library + (LDDL) is part of HELM + and contains a set of + resources expressed in λδ.
      +
        +
      • Contents: + Landau's "Grundlagen + der Analysis" (from + Jutting's specification in Automath).
        +
        • +
      + + +
      + [Helena Logo] Helena + is a λδ + processor, + 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 below.
      +
        +
      +
        +
      • Version 0.8.2. + In + progress.
        +
        • +
      +
        +
      • Version 0.8.1 + (2010-11). + Exploits a subset of "complete_rg" λδ as the + 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) + -
        • -
      -
        -
      • Version 0.8.0 (2009-09). Supports -"basic_rg" λδ with naive implementation of impredicative sort -inclusion. Features -importation from Automath -and exportation to XML. [Svn -revision: 10304] (archived -source code)
        -
          -
        • 2009-09. -Jutting's specification of Landau's "Grundlagen -der -Analysis" enters λδ Digital Library.
          -
          • -
        • 2009-06. -Jutting's specification of Landau's "Grundlagen -der -Analysis" is -successfully processed, enabling sort inclusion.
          • -
        -
        • -
      -

      Other resources [Butterfly]

      - -
        -
      • A Jed mode for -editing ".hln" files (containing λδ textual syntax): helena.sl -(revised 2010-11).
        • -
      - -
        -
      • A logo for "basic" λδ: bld.pdf (revised 2008-07).
        -
        • -
      -
      -
      -[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
      -
      -Last update 2012-02-21 by Ferruccio -Guidi
      -
- +computer + math systems. + + + +
    +
  • Version 0.8.0 (2009-09). + Supports + "basic_rg" λδ with naive implementation of + impredicative sort + inclusion. Features + importation from Automath + and exportation to XML. + [Svn + revision: 10304] (archived + source code)
    +
      +
    • 2009-09. + Jutting's specification of Landau's "Grundlagen + der + Analysis" enters λδ Digital Library.
      +
      • +
    • 2009-06. + Jutting's specification of Landau's "Grundlagen + der + Analysis" is + successfully processed, enabling sort inclusion.
      • +
    +
    • +
+

Other resources [Butterfly]

+ +
    +
  • A Jed mode + for + editing ".hln" files (containing λδ textual syntax): helena.sl + (revised 2010-11).
    • +
+ +
    +
  • A logo for "basic" λδ: bld.pdf + (revised 2008-07).
    +
    • +
+
+
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+ Last update 2012-02-24 by Ferruccio + Guidi
+
+