<page xmlns="http://lambdadelta.info/"
description = "\lambda\delta home page"
title = "\lambda\delta home page"
- head = "The Formal System λδ (\lambda\delta)"
+ logo = "crux"
+ head = "The Formal Systems of the λδ (\lambda\delta) Family"
>
<sitemap name="sitemap"/>
<section5 name="tools">Tools</section5>
- <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
+ <subsection name="osn"><img logo="osn"/>Open Symbolic Notation</subsection>
+
<body>
- The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
- and contains resources expressed in λδ.
+ 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 <rlink to="osn/">OSN web site</rlink>.
</body>
- <news date="Contents:">
- Landau's "Grundlagen der Analysis"
- (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
- </news>
- <news date="Access:">
- <rlink to="static/lddl/">static pages</rlink> (updated <date date="2012-10"/>),
- <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <date date="2012-10"/>),
- <rlink to="xml/">HELM server URL</rlink> (updated <date date="2012-10"/>).
- </news>
- <news date="Examples:">
- <rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
- Grundlagen's definition "t234"</rlink>
- (in "basic_rg" λδ),
- <rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
- Grundlagen's definition "t234"</rlink>
- (in "complete_rg" λδ).
- </news>
- <subsection name="helena"><helena-icon/>Helena</subsection>
+
+ <subsection name="helena"><img logo="helena"/>Helena</subsection>
+
<body>
- Helena is a λδ processor,
+ Helena is a processor for the systems of the λδ family,
implemented in <link to="http://caml.inria.fr/">Caml</link>
as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> 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.
</body>
<body>
The processor source code is available in the directory
of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
The Svn revisions containing the stable versions of Helena are indicated next.
</body>
- <news date="Version 0.8.2.">
- In progress.
- </news>
- <news date="Version 0.8.1 (2010-11).">
- Exploits a subset of "complete_rg" λδ as the intermediate language.
+
+ <topitem name="v3">
+ <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
+ Supports exportation to λProlog
+ (two formats for ELPI,
+ and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
+ Employs optimized conditional compilation through
+ <link to="http://camlp5.gforge.inria.fr/">camlp5</link> 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] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
+ <list><item>
+ <notice class="gamma" notice="2015-06."/>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in a λProlog implementation of λδ version 3.
+ </item></list>
+ </topitem>
+
+ <topitem name="v2">
+ <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
+ Uses λδ version 3 with layer variables as core language.
+ Supports exportation to Gallina
+ (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
+ and to Grafite
+ (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
+ The overall validation speed of the "Grundlagen der Analysis"
+ increases of 34% with respect to version 0.8.1.
+ <rlink to="html/documentation.html#ldJ3a">Documentation (J3a)</rlink>.
+ [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
+ <list><item>
+ The specification of Landau's "Grundlagen der Analysis"
+ for <link to="http://coq.inria.fr/">Coq 8</link>:
+ <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
+ (revised <notice class="gamma" notice="2015-02"/>).
+ </item><item>
+ The specification of Landau's "Grundlagen der Analysis"
+ for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
+ <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
+ (revised <notice class="gamma" notice="2015-02"/>).
+ </item><item>
+ The corrected specification of Landau's "Grundlagen der Analysis":
+ <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
+ (revised <notice class="gamma" notice="2014-12"/>).
+ </item><item>
+ <notice class="gamma" notice="2015-02."/>
+ The translated specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in CC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
+ </item><item>
+ <notice class="gamma" notice="2014-12."/>
+ The corrected specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in λδ version 3.
+ </item></list>
+ </topitem>
+
+ <topitem name="v1">
+ <notice class="beta" notice="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] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
+ [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
for editing ".hln" files (containing λδ textual syntax):
<rlink to="download/helena.sl">helena.sl</rlink>
- (revised <date date="2010-11"/>).
+ (revised <notice class="alpha" notice="2010-11"/>).
</item><item>
- <date date="2009-12."/>
+ <notice class="beta" notice="2009-12."/>
Helena appears in F. Wiedijk's
<link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
index of computer math systems</link>.
</item></list>
- </news>
- <news date="Version 0.8.0 (2009-09).">
- Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+ </topitem>
+
+ <topitem name="v0">
+ <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
+ Supports λδ version 2 with naive implementation of impredicative sort inclusion.
Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
and exportation to <link to="http://www.w3.org/XML/">XML</link>.
- <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
+ <rlink to="html/documentation.html#ldR2a">Documentation (R2a)</rlink>.
[Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
for editing ".aut" files
(containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
<rlink to="download/automath.sl">automath.sl</rlink>
- (revised <date date="2008-07"/>).
+ (revised <notice class="gamma" notice="2008-07"/>).
</item><item>
- <date date="2009-09."/>
+ <notice class="beta" notice="2009-09."/>
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
</item><item>
- <date date="2009-06."/>
+ <notice class="beta" notice="2009-06."/>
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
</item></list>
- </news>
+ </topitem>
+
+ <subsection name="lddl"><img logo="lddl"/>λδ Digital Library (LDDL)</subsection>
+
+ <body>
+ The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
+ and contains resources expressed in the systems of the λδ family.
+ </body>
+ <topitem name="contents">
+ <notice class="alpha" notice="Contents:"/>
+ Landau's "Grundlagen der Analysis"
+ (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
+ </topitem>
+ <topitem name="access">
+ <notice class="alpha" notice="Access:"/>
+ <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
+ <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
+ <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
+ </topitem>
+ <topitem name="examples">
+ <notice class="alpha" notice="Examples:"/>
+ <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ Grundlagen's definition "t234"</rlink>
+ in λδ version 4.
+ </topitem>
+
<footer/>
</page>