X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=cb9b23247edeb484cfdd1f099750506ba2d81ebb;hb=c0d87c3cdf879f61aa53e91f43580e9815ae7190;hp=7785bbf75cf770cdb930d339558caeb21001bcbb;hpb=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80;p=helm.git diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 7785bbf75..cb9b23247 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,26 +1,22 @@ - - - - lambdadelta home page + + + + + λδ home page + - - - - + +

- [Crux Logo] -

The Formal System λδ (lambdadelta)
+ [Crux Logo] +

The Formal System λδ (\lambda\delta)

Towards the unification of terms, types, environments and contexts

- [Separator]
- + [Separator]
+
@@ -40,21 +36,16 @@

Computer-checked formal - specifications [Butterfly]

+ specifications [Butterfly] Resource - 1 below provides for the statically generated natural language + 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 + for the dynamically generated natural language representation of - λδ meta-theory (powered by the HELM + λδ meta-theory (powered by the HELM rendering engine).
Remarkably, λδ was born and developed in the digital format of resource 3 @@ -64,51 +55,42 @@ paper (as it happens for most currently digitalized Mathematics).
    -
  1. F. Guidi: lambdadelta +
  2. F. Guidi: lambdadelta (revised 2011-09). Formal - specification for Matita 0.5 + specification for Matita 0.5 (HTML pages generated by the HELM - rendering engine)
    + rendering engine) Here are the most relevant theorems proved in the formal specification:
    3. -
  3. F. Guidi: lambdadelta +
  4. F. Guidi: lambdadelta (revised 2011-09). Formal - specification for Matita 0.5 (HELM directory).
    -
    + specification for Matita 0.5 (HELM directory).
    + Currently, the HELM rendering engine is offline.
    +
    5. -
  5. F. Guidi: lambdadelta_1 - (revised 2011-09). +
  6. F. Guidi: lambdadelta_1 + (revised 2012-10). Formal specification for Coq 7.3.1 @@ -139,52 +116,35 @@ Formal proof scripts). BibTeX entry.
-

Tools [Butterfly]

- [Crux Logo] The λδ +

Tools [Butterfly]

+ [Crux Logo] The λδ Digital Library - (LDDL) is part of HELM + (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).
    + Jutting's specification in Automath).

- [Helena Logo] Helena + [Helena Logo] Helena is a λδ processor, implemented in Caml @@ -194,10 +154,8 @@ href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.ht 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 + 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 @@ -215,19 +173,16 @@ href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk% intermediate language. Features importation from ".hln" files containing λδ textual syntax. - The overall validation speed of the "Grundlagen + The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. [Svn - revision: 11032] (archived + revision: 11032] (archived source code)
    -
  • Version 0.8.0 (2009-09). +
  • Version 0.8.0 (2009-09). Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion. Features - importation from Automath + importation from Automath and exportation to XML. [Svn - revision: 10304] (archived + revision: 10304] (archived source code)
    • 2009-09. - Jutting's specification of Landau's "Grundlagen + Jutting's specification of Landau's "Grundlagen der Analysis" enters λδ Digital Library.
    • 2009-06. - Jutting's specification of Landau's "Grundlagen + Jutting's specification of Landau's "Grundlagen der Analysis" is - successfully processed, enabling sort inclusion.
      • + successfully processed, enabling sort inclusion.
-

Other resources [Butterfly]

+

Other resources [Butterfly]

  • A Jed mode for - editing ".hln" files (containing λδ textual syntax): helena.sl + editing ".hln" files (containing λδ textual syntax): helena.sl (revised 2010-11).
@@ -306,20 +244,12 @@ computer

- [Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]

- Last update 2012-12-01 by Ferruccio + Last update 2014-02-22 by Ferruccio Guidi
- - + +