+ Helena is a processor for the systems of the λδ family,
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.
+ meant for testing both their stable and unstable features.
+
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.3 (2015-12).
+ Supports exportation to λProlog
+ (two formats for ELPI,
+ and two formats for Teyjus).
+ Employs optimized conditional compilation through
+ camlp5 code preprocessor (pa_macro)
+ to reduce a performance loss, which is expected to disappear
+ by employing a different code preprocessor.
+ Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
+ +3% with optimized compilation, +5% without optimized compilation.
+ [Svn revision: 13108] (archived source code).
+
+ -
+ 2015-06.
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in a λProlog implementation of λδ version 3.
+
+
+
+
+
+ -
+ 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 CC 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).
- -
+
-
A Jed mode
for editing ".aut" files
(containing Automath textual syntax):
automath.sl
(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.
+
+
+
+
λδ Digital Library (LDDL)
+
+ The λδ Digital Library is part of
HELM
+ and contains resources expressed in the systems of the λδ family.
+
+
+ -
+ Contents:
+ Landau's "Grundlagen der Analysis"
+ (from Jutting's specification in Automath).
-
-
+
+
+
+
@@ -226,6 +302,6 @@
-
Last update: Tue, 04 Nov 2014 16:21:22 +0100
-
+
Last update: Fri, 24 Nov 2017 21:00:00 +0100
+