X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=590ea923f9cba9ee1843b381f280cdf868dbfb9b;hb=d48d412796a295256c048256c8f7a843e3406980;hp=7785bbf75cf770cdb930d339558caeb21001bcbb;hpb=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80;p=helm.git diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 7785bbf75..590ea923f 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,325 +1,271 @@ - - + + + - - lambdadelta home page - - - + + + + + + \lambda\delta home page + + + + - -
-
- [Crux Logo] -

The Formal System λδ (lambdadelta)
-

-

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

- [Separator]
- + +
+ + [lambdadelta home] + +
+
The Formal System λδ (\lambda\delta)
+
+ [Spacer] +
+
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + documentation + + implementation + (specifications - library - Helena)
+ Foreword + + Milestones + + Version 2 + + Version 2 + (Background - Core - Applications)
+ Notice + + Visibility + + Version 1 + + Version 1 + +
+
+
+ +
Computer-checked formal specifications [spacer] +
+
+ λδ comes in several versions listed in the following table, + which includes the major milestones: +
+
+ - + + + + + + + + + + - + + + + + + + + + + + + + + +
- - - -
    -
  • Resources
    -
    • -
+ 		versionnamedeveloped withstagestartedannouncedreleaseddismissed
+ Version 2 -

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: lambdadelta - (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: lambdadelta - (revised 2011-09). - Formal - specification for Matita 0.5 (HELM directory).
    -
    -
    3. -
  3. F. Guidi: lambdadelta_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 λδ: crux_177.png - (revised 2012-09).
    -
    • -
+ 		"basic_2" + Matita 0.99.2 "A"April 2011July 2014Planned in 2014Not planned yet
+ Version 1 + "basic_1" + Coq 7.3.1 + + May 2004January 2006November 2006May 2008
-
- [Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
-
- Last update 2012-12-01 by Ferruccio - Guidi
- + +
Tools [spacer] +
+ +
+ [Crux logo] λδ Digital Library (LDDL)
+
+ The λδ Digital Library is part of HELM + and contains resources expressed in λδ. +
+ + + + +
+ [Helena logo] Helena
+
+ 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 next. +
+ + + +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+