X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=8d16e68904737e59463c82497f9bbc47a73f0f4d;hb=e17e8a363454a2a1ce9629a5f99d72196d8592a1;hp=b7e1d0a8a18992351e5c8c9cc540ae14e02f4998;hpb=cc57e6f6528ccc871a4d52d2ce4859c4a76fc0ca;p=helm.git diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html index b7e1d0a8a..8d16e6890 100644 --- a/helm/www/lambda_delta/implementation.html +++ b/helm/www/lambda_delta/implementation.html @@ -1,275 +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 with the proof assistant Matita 0.5 (HTML pages generated -by the HELM -rendering engine)
    -Here are the most relevant theorems proved in the formal specification: -
      -
    • Confluence -of -reduction (Church-Rosser property).
      • -
    • Correctness -of -types.
      • -
    • Uniqueness -of -types -up -to -conversion.
      -
      • -
    • Subject -reduction -of -the -type -assignment.
      • -
    • Strong -normalization -of -the -typed -terms.
      • -
    • Decidability -of -the -type -inference -problem.
      + + + 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).
        +
        • +
      + +
      - - - -
    • F. Guidi: lambda_delta -(revised 2011-09). Formal -specification with the proof assistant Matita 0.5 (HELM directory).
      -
      -
      • -
    • F. Guidi: lambda_delta_1 (revised 2011-09). -Formal specification with the proof assistant Coq 7.3.1 (source -proof scripts). BibTeX entry.
      -
      • - -

      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]

      - [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/lambda_delta/ -of the HELM Svn -repository. The Svn revisions containing the stable versions -of  Helena are indicated below.
      -
        -
      • 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 2011-09-09 by Ferruccio -Guidi
-
- + Last update 2012-02-24 by Ferruccio + Guidi
+ +