- The λδ Digital Library is part of
HELM
- and contains resources expressed in the systems of the λδ family.
+ Open Symbolic Notation, abbreviated OSN,
+ is an easy and flexible data-interchange text format
+ intended for the lightweight representation of
+ generic abstract syntax trees in the domain of formal languages.
+ Additional information is available at
OSN web site.
@@ -161,7 +143,7 @@
+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.
@@ -182,29 +164,29 @@
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.
@@ -221,13 +203,13 @@
increases of 22% with respect to version 0.8.0.
[Svn revision: 11032] (archived source code).
- -
+
-
A Jed mode
for editing ".hln" files (containing λδ textual syntax):
helena.sl
(revised 2010-11).
- -
+
-
2009-12.
Helena appears in F. Wiedijk's
@@ -245,19 +227,19 @@
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.
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
- -
+
-
2009-06.
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
@@ -265,8 +247,37 @@
+
+
λδ 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).
+
+
+
+
-
+
@@ -291,6 +302,6 @@
-
Last update: Fri, 04 Mar 2016 16:15:58 +0100
+
Last update: Fri, 22 Jul 2016 19:34:08 +0200