X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=9112a8037985ab0da12e3dc852c616d779995338;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=1ae011367aa7c71bbad56ea2c11624b90953f30a;hpb=bda6d964ce9729a694e3fd3ead386ca9f2ca14e3;p=helm.git
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 1ae011367..9112a8037 100644
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -7,41 +7,34 @@
>
- Computer-checked formal specifications
-
- λδ comes in several versions listed in the following table,
- which includes the major milestones:
-
-
-
Tools
- λδ Digital Library (LDDL)
+ λδ Digital Library (LDDL)
The λδ Digital Library is part of HELM
and contains resources expressed in λδ.
-
+
+
Landau's "Grundlagen der Analysis"
(from Jutting's specification in Automath).
-
-
- static pages (updated ),
- data set (updated ),
- HELM server URL (updated ).
-
-
-
+
+
+
+ static pages (updated ),
+ data set (updated ),
+ HELM server URL (updated ).
+
+
+
+
Grundlagen's definition "t234"
- (in "basic_rg" λδ),
-
- Grundlagen's definition "t234"
- (in "complete_rg" λδ).
-
+ in λδ version 4.
+
- Helena
+ Helena
- Helena is a λδ processor,
+ Helena is a processor for λδ,
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.
@@ -52,29 +45,63 @@
of the HELM Svn repository.
The Svn revisions containing the stable versions of Helena are indicated next.
-
- In progress.
-
-
- Exploits a subset of "complete_rg" λδ as the intermediate language.
+
+
+ Uses λδ "Version 3" with layer variables as core language.
+ Supports exportation to Gallina
+ (the specification language of Coq),
+ and to Grafite
+ (the specification language of Matita).
+ The overall validation speed of the "Grundlagen der Analysis"
+ increases of 34% with respect to version 0.8.1.
+ Documentation (J4).
+ [Svn revision: 13035] (archived source code).
+
+ The specification of Landau's "Grundlagen der Analysis"
+ for Coq 8:
+ grundlagen_2.v
+ (revised ).
+
+ The specification of Landau's "Grundlagen der Analysis"
+ for Matita 0.99.2:
+ grundlagen_2.tar.bz2
+ (revised ).
+
+ The corrected specification of Landau's "Grundlagen der Analysis":
+ grundlagen_2.aut
+ (revised ).
+
+
+ The translated specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in λC by Coq 8.4.3.
+
+
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in λδ "Version 3".
+
+
+
+
+ Uses a subset of λδ "Version 4" as 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)
+ [Svn revision: 11032] (archived source code).
A Jed mode
for editing ".hln" files (containing λδ textual syntax):
helena.sl
- (revised ).
+ (revised ).
-
+
Helena appears in F. Wiedijk's
index of computer math systems.
-
-
- Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+
+
+
+ Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
Features importation from Automath
and exportation to XML.
Documentation (R4).
@@ -84,16 +111,16 @@
for editing ".aut" files
(containing Automath textual syntax):
automath.sl
- (revised ).
+ (revised ).
-
+
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
-
+
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
-
+