1 <?xml version="1.0" encoding="UTF-8"?>
3 <page xmlns="http://lambdadelta.info/"
4 description = "\lambda\delta home page"
5 title = "\lambda\delta home page"
6 head = "The Formal Systems of the λδ (\lambda\delta) Family"
8 <sitemap name="sitemap"/>
10 <section5 name="tools">Tools</section5>
12 <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
14 The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
15 and contains resources expressed in the systems of the λδ family.
17 <topitem name="contents">
18 <notice class="alpha" notice="Contents:"/>
19 Landau's "Grundlagen der Analysis"
20 (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
22 <topitem name="access">
23 <notice class="alpha" notice="Access:"/>
24 <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
25 <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
26 <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
28 <topitem name="examples">
29 <notice class="alpha" notice="Examples:"/>
30 <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
31 Grundlagen's definition "t234"</rlink>
35 <subsection name="helena"><helena-icon/>Helena</subsection>
38 Helena is a processor for the systems of the λδ family,
39 implemented in <link to="http://caml.inria.fr/">Caml</link>
40 as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
41 meant for testing both their stable and unstable features.
44 The processor source code is available in the directory
45 <link to="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&rev=0&sc=0">/trunk/helm/software/helena/</link>
46 of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
47 The Svn revisions containing the stable versions of Helena are indicated next.
51 <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
52 Supports exportation to λProlog
53 (two formats for ELPI,
54 and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
55 Employs optimized conditional compilation through
56 <link to="http://camlp5.gforge.inria.fr/">camlp5</link> code preprocessor (pa_macro)
57 to reduce a performance loss, which is expected to disappear
58 by employing a different code preprocessor.
59 Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
60 +3% with optimized compilation, +5% without optimized compilation.
61 [Svn revision: 13108] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
63 <notice class="gamma" notice="2015-06."/>
64 The corrected specification of Landau's "Grundlagen der Analysis"
65 is successfully validated in a λProlog implementation of λδ version 3.
70 <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
71 Uses λδ version 3 with layer variables as core language.
72 Supports exportation to Gallina
73 (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
75 (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
76 The overall validation speed of the "Grundlagen der Analysis"
77 increases of 34% with respect to version 0.8.1.
78 <rlink to="documentation.html#ldJ3a">Documentation (J3a)</rlink>.
79 [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
81 The specification of Landau's "Grundlagen der Analysis"
82 for <link to="http://coq.inria.fr/">Coq 8</link>:
83 <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
84 (revised <notice class="gamma" notice="2015-02"/>).
86 The specification of Landau's "Grundlagen der Analysis"
87 for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
88 <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
89 (revised <notice class="gamma" notice="2015-02"/>).
91 The corrected specification of Landau's "Grundlagen der Analysis":
92 <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
93 (revised <notice class="gamma" notice="2014-12"/>).
95 <notice class="gamma" notice="2015-02."/>
96 The translated specification of Landau's "Grundlagen der Analysis"
97 is successfully validated in CC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
99 <notice class="gamma" notice="2014-12."/>
100 The corrected specification of Landau's "Grundlagen der Analysis"
101 is successfully validated in λδ version 3.
106 <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
107 Uses a subset of λδ version 4 as intermediate language.
108 Features importation from ".hln" files containing λδ textual syntax.
109 The overall validation speed of the "Grundlagen der Analysis"
110 increases of 22% with respect to version 0.8.0.
111 [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
113 A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
114 for editing ".hln" files (containing λδ textual syntax):
115 <rlink to="download/helena.sl">helena.sl</rlink>
116 (revised <notice class="alpha" notice="2010-11"/>).
118 <notice class="beta" notice="2009-12."/>
119 Helena appears in F. Wiedijk's
120 <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
121 index of computer math systems</link>.
126 <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
127 Supports λδ version 2 with naive implementation of impredicative sort inclusion.
128 Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
129 and exportation to <link to="http://www.w3.org/XML/">XML</link>.
130 <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
131 [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
133 A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
134 for editing ".aut" files
135 (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
136 <rlink to="download/automath.sl">automath.sl</rlink>
137 (revised <notice class="gamma" notice="2008-07"/>).
139 <notice class="beta" notice="2009-09."/>
140 Jutting's specification of Landau's "Grundlagen der Analysis"
141 enters λδ Digital Library.
143 <notice class="beta" notice="2009-06."/>
144 Jutting's specification of Landau's "Grundlagen der Analysis"
145 is successfully processed, enabling sort inclusion.