+ 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.
+
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.
-
+
-
- Version 0.8.2.
- In progress.
-
+ Version 0.8.2 (2015-02).
+ 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 (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 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.
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in λδ "Version 3".
+
+
+
-
+
-
- Version 0.8.1 (2010-11).
- Exploits a subset of "complete_rg" λδ as the intermediate language.
+ Version 0.8.1 (2010-11).
+ 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).
-
+
-
+
-
- Version 0.8.0 (2009-09).
- Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+ Version 0.8.0 (2009-09).
+ Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
Features importation from Automath
and exportation to XML.
- Documentation (R4).
+ Documentation (R2a).
[Svn revision: 10304] (archived source code).
-
@@ -225,22 +228,22 @@
for editing ".aut" files
(containing Automath textual syntax):
automath.sl
- (revised 2008-07).
+ (revised 2008-07).
-
- 2009-09.
+ 2009-09.
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
-
- 2009-06.
+ 2009-06.
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
-
+
-
+
@@ -266,6 +269,6 @@
-
Last update: Thu, 02 Oct 2014 22:32:44 +0200
-