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 white">
40 <a href="http://lambdadelta.info/specification.html">specification</a>
42 <td class="snnn capitalize italic white">
45 <td class="snnn capitalize italic white">
48 <td class="snns capitalize italic orange">
49 <a href="http://lambdadelta.info/documentation.html">documentation</a>
51 <td class="snns capitalize italic green">
52 <a href="http://lambdadelta.info/implementation.html">implementation</a>
54 <td class="ssnn capitalize italic green">
59 <td class="snns capitalize sky">
60 <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
62 <td class="snns capitalize magenta">
63 <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
65 <td class="snns capitalize white">
66 <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
68 <td class="snnn capitalize white">(<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="snnn capitalize white">
72 <td class="snns capitalize orange">
73 <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
75 <td class="snns capitalize green">
76 <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
78 <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
81 <td class="snss capitalize sky">
82 <a href="http://lambdadelta.info/index.html#citations">citations</a>
84 <td class="snss capitalize magenta">
85 <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
87 <td class="snss capitalize white">
88 <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
90 <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
91 <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
92 <td class="snss capitalize orange">
93 <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
95 <td class="snss capitalize green">
96 <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
98 <td class="sssn capitalize green">
105 <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" />
107 <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
108 <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
109 <div xmlns:ld="http://lambdadelta.info/" class="text">
110 The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
111 and contains resources expressed in λδ.
113 <ul xmlns:ld="http://lambdadelta.info/" id="contents">
115 <span class="emph alpha">Contents:</span>
116 Landau's "Grundlagen der Analysis"
117 (from Jutting's specification in <a href="http://www.win.tue.nl/automath/">Automath</a>).
120 <ul xmlns:ld="http://lambdadelta.info/" id="access">
122 <span class="emph alpha">Access:</span>
123 <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph gamma">2015-01</span>),
124 <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph gamma">2014-12</span>),
125 <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph gamma">2014-12</span>).
128 <ul xmlns:ld="http://lambdadelta.info/" id="examples">
130 <span class="emph alpha">Examples:</span>
131 <a href="http://lambdadelta.info/static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
132 Grundlagen's definition "t234"</a>
136 <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
137 <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
138 <div xmlns:ld="http://lambdadelta.info/" class="text">
139 Helena is a processor for λδ,
140 implemented in <a href="http://caml.inria.fr/">Caml</a>
141 as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
142 meant for testing the stable features of the calculus as well as the unstable ones.
144 <div xmlns:ld="http://lambdadelta.info/" class="text">
145 The processor source code is available in the directory
146 <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>
147 of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
148 The Svn revisions containing the stable versions of Helena are indicated next.
150 <ul xmlns:ld="http://lambdadelta.info/" id="v2">
152 <span class="emph gamma">Version 0.8.2 (2015-02).</span>
153 Uses λδ "Version 3" with layer variables as core language.
154 Supports exportation to Gallina
155 (the specification language of <a href="http://coq.inria.fr/">Coq</a>),
157 (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
158 The overall validation speed of the "Grundlagen der Analysis"
159 increases of 34% with respect to version 0.8.1.
160 <a href="http://lambdadelta.info/documentation.html#ldJ3a">Documentation (J3a)</a>.
161 [Svn revision: 13035] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>).
164 The specification of Landau's "Grundlagen der Analysis"
165 for <a href="http://coq.inria.fr/">Coq 8</a>:
166 <a href="http://lambdadelta.info/download/grundlagen_2.v">grundlagen_2.v</a>
167 (revised <span class="emph gamma">2015-02</span>).
170 The specification of Landau's "Grundlagen der Analysis"
171 for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
172 <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
173 (revised <span class="emph gamma">2015-02</span>).
176 The corrected specification of Landau's "Grundlagen der Analysis":
177 <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
178 (revised <span class="emph gamma">2014-12</span>).
181 <span class="emph gamma">2015-02.</span>
182 The translated specification of Landau's "Grundlagen der Analysis"
183 is successfully validated in λC by <a href="http://coq.inria.fr/">Coq 8.4.3</a>.
186 <span class="emph gamma">2014-12.</span>
187 The corrected specification of Landau's "Grundlagen der Analysis"
188 is successfully validated in λδ "Version 3".
193 <ul xmlns:ld="http://lambdadelta.info/" id="v1">
195 <span class="emph beta">Version 0.8.1 (2010-11).</span>
196 Uses a subset of λδ "Version 4" as intermediate language.
197 Features importation from ".hln" files containing λδ textual syntax.
198 The overall validation speed of the "Grundlagen der Analysis"
199 increases of 22% with respect to version 0.8.0.
200 [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>).
203 A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
204 for editing ".hln" files (containing λδ textual syntax):
205 <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
206 (revised <span class="emph alpha">2010-11</span>).
209 <span class="emph beta">2009-12.</span>
210 Helena appears in F. Wiedijk's
211 <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
212 index of computer math systems</a>.
217 <ul xmlns:ld="http://lambdadelta.info/" id="v0">
219 <span class="emph beta">Version 0.8.0 (2009-09).</span>
220 Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
221 Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
222 and exportation to <a href="http://www.w3.org/XML/">XML</a>.
223 <a href="http://lambdadelta.info/documentation.html#ldR2a">Documentation (R2a)</a>.
224 [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
227 A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
228 for editing ".aut" files
229 (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
230 <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
231 (revised <span class="emph gamma">2008-07</span>).
234 <span class="emph beta">2009-09.</span>
235 Jutting's specification of Landau's "Grundlagen der Analysis"
236 enters λδ Digital Library.
239 <span class="emph beta">2009-06.</span>
240 Jutting's specification of Landau's "Grundlagen der Analysis"
241 is successfully processed, enabling sort inclusion.
247 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
249 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
252 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
253 <a href="http://validator.w3.org/check?uri=referer">
254 <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
256 <a href="http://jigsaw.w3.org/css-validator/check/referer">
257 <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
259 <a href="http://www.w3.org/XML/">
260 <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
262 <a href="http://www.w3.org/Graphics/PNG/">
263 <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
265 <a href="http://www.anybrowser.org/campaign/">
266 <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
269 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
272 <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 02 Sep 2015 17:59:06 +0200</div>