1 <?xml version="1.0" encoding="UTF-8"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
5 <meta http-equiv="Content-Language" content="en-us" />
6 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
7 <meta http-equiv="Content-Style-Type" content="text/css" />
8 <meta name="author" content="Ferruccio Guidi" />
9 <meta name="description" content="\lambda\delta home page" />
10 <title>\lambda\delta home page</title>
11 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
12 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
13 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
14 <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
18 <a href="http://lambdadelta.info/">
19 <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
22 <div class="head1">The Formal System λδ (\lambda\delta)</div>
24 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
26 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
29 <div xmlns:ld="http://lambdadelta.info/" class="text">
30 <table cellpadding="4" cellspacing="0">
33 <td class="snns capitalize italic sky">
34 <a href="http://lambdadelta.info/index.html">home</a>
36 <td class="snns capitalize italic magenta">
37 <a href="http://lambdadelta.info/news.html">news</a>
39 <td class="snns capitalize italic orange">
40 <a href="http://lambdadelta.info/documentation.html">documentation</a>
42 <td class="snns capitalize italic green">
43 <a href="http://lambdadelta.info/specification.html">specification</a>
45 <td class="snnn capitalize italic green">
48 <td class="snns capitalize italic green">
49 <a href="http://lambdadelta.info/implementation.html">implementation</a>
51 <td class="ssnn capitalize italic green">
56 <td class="snns capitalize sky">
57 <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
59 <td class="snns capitalize magenta">
60 <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
62 <td class="snns capitalize orange">
63 <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
65 <td class="snns capitalize green">
66 <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
68 <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
69 <td class="snns capitalize green">
70 <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
72 <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
75 <td class="snss capitalize sky">
76 <a href="http://lambdadelta.info/index.html#citations">citations</a>
78 <td class="snss capitalize magenta">
79 <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
81 <td class="snss capitalize orange">
82 <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
84 <td class="snss capitalize green">
85 <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
87 <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
88 <td class="snss capitalize green">
89 <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
91 <td class="sssn capitalize green">
98 <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="tools">Tools <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
100 <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
101 <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
102 <div xmlns:ld="http://lambdadelta.info/" class="text">
103 The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
104 and contains resources expressed in λδ.
106 <ul xmlns:ld="http://lambdadelta.info/" id="contents">
108 <span class="emph alpha">Contents:</span>
109 Landau's "Grundlagen der Analysis"
110 (from Jutting's specification in <a href="http://www.win.tue.nl/automath/">Automath</a>).
113 <ul xmlns:ld="http://lambdadelta.info/" id="access">
115 <span class="emph alpha">Access:</span>
116 <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph gamma">2015-01</span>),
117 <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph gamma">2014-12</span>),
118 <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph gamma">2014-12</span>).
121 <ul xmlns:ld="http://lambdadelta.info/" id="examples">
123 <span class="emph alpha">Examples:</span>
124 <a href="http://lambdadelta.info/static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
125 Grundlagen's definition "t234"</a>
129 <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
130 <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
131 <div xmlns:ld="http://lambdadelta.info/" class="text">
132 Helena is a processor for λδ,
133 implemented in <a href="http://caml.inria.fr/">Caml</a>
134 as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
135 meant for testing the stable features of the calculus as well as the unstable ones.
137 <div xmlns:ld="http://lambdadelta.info/" class="text">
138 The processor source code is available in the directory
139 <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&rev=0&sc=0">/trunk/helm/software/helena/</a>
140 of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
141 The Svn revisions containing the stable versions of Helena are indicated next.
143 <ul xmlns:ld="http://lambdadelta.info/" id="v2">
145 <span class="emph gamma">Version 0.8.2 (2014-12).</span>
146 Uses λδ "Version 3" with layer variables as core language.
147 Supports exportation to Grafite
148 (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
149 The overall validation speed of the "Grundlagen der Analysis"
150 increases of 34% with respect to version 0.8.1.
151 [Svn revision: 13005] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>)
154 The specification of Landau's "Grundlagen der Analysis"
155 for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
156 <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
157 (revised <span class="emph gamma">2014-12</span>).
160 The corrected specification of Landau's "Grundlagen der Analysis":
161 <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
162 (revised <span class="emph gamma">2014-12</span>).
165 <span class="emph gamma">2014-12.</span>
166 The corrected specification of Landau's "Grundlagen der Analysis"
167 is successfully validated in λδ "Version 3".
172 <ul xmlns:ld="http://lambdadelta.info/" id="v1">
174 <span class="emph beta">Version 0.8.1 (2010-11).</span>
175 Uses a subset of λδ "Version 4" as intermediate language.
176 Features importation from ".hln" files containing λδ textual syntax.
177 The overall validation speed of the "Grundlagen der Analysis"
178 increases of 22% with respect to version 0.8.0.
179 [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
182 A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
183 for editing ".hln" files (containing λδ textual syntax):
184 <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
185 (revised <span class="emph alpha">2010-11</span>).
188 <span class="emph beta">2009-12.</span>
189 Helena appears in F. Wiedijk's
190 <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
191 index of computer math systems</a>.
196 <ul xmlns:ld="http://lambdadelta.info/" id="v0">
198 <span class="emph beta">Version 0.8.0 (2009-09).</span>
199 Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
200 Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
201 and exportation to <a href="http://www.w3.org/XML/">XML</a>.
202 <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
203 [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
206 A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
207 for editing ".aut" files
208 (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
209 <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
210 (revised <span class="emph gamma">2008-07</span>).
213 <span class="emph beta">2009-09.</span>
214 Jutting's specification of Landau's "Grundlagen der Analysis"
215 enters λδ Digital Library.
218 <span class="emph beta">2009-06.</span>
219 Jutting's specification of Landau's "Grundlagen der Analysis"
220 is successfully processed, enabling sort inclusion.
226 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
228 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
231 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
232 <a href="http://validator.w3.org/check?uri=referer">
233 <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
235 <a href="http://jigsaw.w3.org/css-validator/check/referer">
236 <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
238 <a href="http://www.w3.org/XML/">
239 <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
241 <a href="http://www.w3.org/Graphics/PNG/">
242 <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
244 <a href="http://www.anybrowser.org/campaign/">
245 <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
248 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
251 <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:44 +0100</div>