+ 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 (2014-12).
+ Uses λδ "Version 3" with layer variables as core language.
+ Supports exportation 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)
-
The specification of Landau's "Grundlagen der Analysis"
@@ -158,17 +162,17 @@
(revised 2014-12).
-
- 2014-12.
+ 2014-12.
The corrected specification of Landau's "Grundlagen der Analysis"
is successfully validated in λδ "Version 3".
-
+
-
+
-
- Version 0.8.1 (2010-11).
- Uses a subset of λδ "Version 4" 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.
@@ -181,17 +185,17 @@
(revised 2010-11).
-
- 2009-12.
+ 2009-12.
Helena appears in F. Wiedijk's
index of computer math systems.
-
+
-
+
-
- Version 0.8.0 (2009-09).
+ Version 0.8.0 (2009-09).
Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
Features importation from Automath
and exportation to XML.
@@ -206,19 +210,19 @@
(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.
-
+
-
+
@@ -244,6 +248,6 @@
-
Last update: Fri, 26 Dec 2014 16:35:05 +0100
-