X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;fp=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=c046df27de484088ea1564cf8136a7f2400ec928;hb=fba2975ffd09ffb30a60500725c9991421445f37;hp=0000000000000000000000000000000000000000;hpb=b4240d93f7fd4c3e60d3495dc558edfc0e0f48e7;p=helm.git diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html new file mode 100644 index 000000000..c046df27d --- /dev/null +++ b/helm/www/lambda_delta/implementation.html @@ -0,0 +1,274 @@ + + + + + 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-TYPES +(revised 2008-06). 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: + +
    2. +
  2. F. Guidi: LAMBDA-TYPES +(revised 2008-06). Formal +specification with the proof assistant Matita 0.5 (HELM directory).
    +
    +
    3. +
  3. F. Guidi: LAMBDA-TYPES (revised 2008-03). +Formal specification with the proof assistant 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/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 2010-12-14 by Ferruccio +Guidi
+
+ +