X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=c86890da2629845737637a56094d1735f48d5ebf;hb=32def68dd99ad5f20f001e3e76b51afa6f69dec5;hp=b11b5b995bf77582a16d8038bff3806142e295e5;hpb=fe00a22101acb7995f8488a4434c4046bc540af0;p=helm.git
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index b11b5b995..c86890da2 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -36,15 +36,18 @@
news
|
-
- documentation
- |
-
+ |
specification
|
-
+ |
|
+
+
+ |
+
+ documentation
+ |
implementation
|
@@ -59,13 +62,16 @@
milestones
|
+
+ version 2
+ |
+ (background - core - applications) |
+
+
+ |
version 2
|
-
- version 2
- |
- (background - core - applications) |
library
|
@@ -78,13 +84,14 @@
visibility
|
+
+ version 1
+ |
+ (background - core) |
+ (static HELM directory) |
version 1
|
-
- version 1
- |
- (static HELM directory) |
helena
|
@@ -142,24 +149,38 @@
-
- Version 0.8.2 (2014-12).
+ Version 0.8.2 (2015-02).
Uses λδ "Version 3" with layer variables as core language.
- Supports exportation to Grafite
+ 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.
- [Svn revision: 13005] (archived source code)
+ Documentation (J3a).
+ [Svn revision: 13035] (archived source code).
-
The specification of Landau's "Grundlagen der Analysis"
+ for Coq 8:
+ grundlagen_2.v
+ (revised 2015-02).
+
+ -
+ The specification of Landau's "Grundlagen der Analysis"
for Matita 0.99.2:
grundlagen_2.tar.bz2
- (revised 2014-12).
+ (revised 2015-02).
-
The corrected specification of Landau's "Grundlagen der Analysis":
grundlagen_2.aut
(revised 2014-12).
+
+ -
+ 2015-02.
+ The translated specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in λC by Coq 8.4.3.
-
2014-12.
@@ -176,7 +197,7 @@
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).