1 <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
4 <meta content="text/html; charset=UTF-8" http-equiv="content-type">
5 <title>lambda_delta home page</title>
6 <meta content="Ferruccio Guidi" name="author">
7 <meta content="The formal system lambda_delta" name="description">
8 <link rel="shortcut icon" href="download/crux_16.ico">
11 <div style="text-align: center;">
13 <a href="http://lambda-delta.info"><img alt="[Crux Logo]"
14 title="The Crux" src="download/crux_32.png" style="border: 0px
15 solid ; width: 32px; height: 32px;"></a>
16 <h1>The Formal System λδ (lambda_delta)<br>
18 <h2>Towards the unification of terms, types, environments and
20 <img style="width: 95%; height: 4px;" alt="[Separator]"
21 title="Separator" src="download/rainbow.png"><br>
22 <table style="text-align: left; width: 95%; margin-left: auto;
23 margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
26 <td style="vertical-align: top;">
28 <li><a href="index.html">Foreword</a></li>
31 <li><a href="news.html">News</a></li>
34 <li><a href="documentation.html">Papers</a></li>
41 <td style="vertical-align: top; text-align: left;">
42 <h3 style="text-align: right;">Computer-checked formal
43 specifications <img style="width: 37px; height: 37px;"
44 alt="[Butterfly]" title="Butterfly"
45 src="download/b9.png"></h3>
46 <span style="font-weight: bold;">Resource
47 1</span> below provides for the statically generated <span
48 style="font-weight: bold;">natural language
49 representation</span> of
50 λδ meta-theory (faster rendering w.r.t. resource 2 below).<br>
51 <span style="font-weight: bold;">Resource 2</span> below
53 for the dynamically generated <span style="font-weight:
55 language representation</span> of
56 λδ meta-theory (powered by the <a
57 href="http://helm.cs.unibo.it/">HELM</a>
58 rendering engine).<br>
59 Remarkably, λδ was born and developed in the digital
60 format of <span style="font-weight: bold;">resource 3</span>
61 below, which is not the
62 formal counterpart of some informal material previously
64 paper (as it happens for most currently digitalized
67 <li><a name="static"></a>F. Guidi: <a
68 style="font-style: italic;"
69 href="static/matita/lambda_delta/">lambda_delta</a>
70 (revised <span style="font-weight: bold;">2011-09</span>).
73 href="http://matita.cs.unibo.it/">Matita</a> 0.5
75 by the <a href="http://helm.cs.unibo.it/">HELM</a>
77 Here are the most relevant theorems proved in the
81 href="static/matita/lambda_delta/Basic_1/pr3/pr3/pr3_confluence.con.html">Confluence
83 reduction</a> (Church-Rosser property).</li>
85 href="static/matita/lambda_delta/Basic_1/ty3/props/ty3_correct.con.html">Correctness
89 href="static/matita/lambda_delta/Basic_1/ty3/props/ty3_unique.con.html">Uniqueness
97 href="static/matita/lambda_delta/Basic_1/ty3/pr3/ty3_sred_pr3.con.html">Subject
104 href="static/matita/lambda_delta/Basic_1/ty3/arity_props/ty3_sn3.con.html">Strong
111 href="static/matita/lambda_delta/Basic_1/ty3/dec/ty3_inference.con.html">Decidability
121 <li><a name="dynamic"></a>F. Guidi: <a
122 style="font-style: italic;"
123 href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambda_delta/">lambda_delta</a>
124 (revised <span style="font-weight: bold;">2011-09</span>).
127 href="http://matita.cs.unibo.it/">Matita</a> 0.5 (<a
128 href="http://helm.cs.unibo.it/">HELM</a> directory).<br>
131 <li><a name="ldp1"></a>F. Guidi: <a
132 href="download/lambda_delta_1.tar.gz"><span
133 style="font-style: italic;">lambda_delta_1</span></a>
134 (revised <span style="font-weight: bold;">2011-09</span>).
136 specification for <span style="font-weight: bold;">Coq
139 proof scripts). <a href="#bibtex">BibTeX entry</a>.<br>
142 <h3 style="text-align: right;">Tools <img style="width:
143 37px; height: 37px;" alt="[Butterfly]"
144 title="Butterfly" src="download/b5.png"></h3>
145 <a name="lddl"></a><img style="width: 32px; height: 32px;"
146 alt="[Crux Logo]" title="The Crux"
147 src="download/crux_32.png"><span style="font-weight:
148 bold;"> </span>The <span style="font-weight: bold;"><span
149 style="text-decoration: underline;">λδ
152 (LDDL)</span></span> is part of <a
153 href="http://helm.cs.unibo.it/">HELM</a>
154 and contains a set of
155 resources expressed in λδ.<br>
157 <li><span style="font-weight: bold;">Contents:</span>
158 Landau's "<span style="font-style: italic;">Grundlagen
159 der Analysis</span>" (from
160 Jutting's specification in <a
161 href="http://www.win.tue.nl/automath/">Automath</a>).<br>
162 <span style="font-weight: bold;"></span></li>
165 <li><span style="font-weight: bold;">Access:</span> <a
166 href="static/lddl/">static pages</a> (updated <span
167 style="font-weight: bold;">2011-09</span>), <a
168 href="download/lddl.tar.bz2">data set</a> (updated <span
169 style="font-weight: bold;">2011-09</span>), <a
170 href="http://lambda-delta.info/xml">HELM server URL</a>
171 (updated <span style="font-weight: bold;">2011-09</span>).</li>
174 <li><span style="font-weight: bold;">Examples:</span> <a
175 href="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
177 "t234"</a> (in "basic_rg" λδ), <a
178 href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
180 "t234"</a> (in "complete_rg" λδ).<br>
184 <a name="helena"></a><span style="font-weight: bold;"><img
185 style="width: 32px; height: 32px;" alt="[Helena Logo]"
186 title="Helena" src="download/helena_32.png"> <span
187 style="text-decoration: underline;">Helena</span></span>
190 implemented in <a href="http://caml.inria.fr/">Caml</a>
192 the <a href="http://helm.cs.unibo.it/">HELM</a> software,
194 testing the stable features of the calculus as well as the
197 The processor source code is available in the directory <a
198 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>
200 href="http://helm.cs.unibo.it/software/index.html">HELM
202 repository</a>. The Svn revisions containing the stable
204 of Helena are indicated below. <br>
206 <li><span style="font-weight: bold;">Version 0.8.2.</span>
212 <li><span style="font-weight: bold;">Version 0.8.1
214 Exploits a subset of "complete_rg" λδ as the
215 intermediate language.
216 Features importation from ".hln" files containing λδ
218 The overall validation speed of the "<span
219 style="font-style: italic;">Grundlagen
221 Analysis</span>" increases of 22% with respect to
224 href="download/helena_0.8.1.tar.gz">archived
227 <li><span style="font-weight: bold;">2009-12.</span>
229 appears in F. Wiedijk's <a
230 href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">index
233 math systems</a>.</li>
238 <li><a style=" font-weight: bold;"
239 href="documentation.html#ldp6">Version 0.8.0</a><span
240 style="font-weight: bold;"> (2009-09).</span>
242 "basic_rg" λδ with naive implementation of
246 href="http://www.win.tue.nl/automath/">Automath</a>
247 and exportation to <a href="http://www.w3.org/XML/">XML</a>.
250 href="download/helena_0.8.0.tar.gz">archived
253 <li><span style="font-weight: bold;">2009-09.</span>
254 Jutting's specification of Landau's "<span
255 style="font-style: italic;">Grundlagen
257 Analysis</span>" enters λδ Digital Library.<br>
258 <span style="font-weight: bold;"></span></li>
259 <li><span style="font-weight: bold;">2009-06.</span>
260 Jutting's specification of Landau's "<span
261 style="font-style: italic;">Grundlagen
264 successfully processed, enabling sort inclusion<span
265 style="font-weight: bold;"></span>.</li>
269 <h3 style="text-align: right;">Other resources <img
270 style="width: 37px; height: 37px;" alt="[Butterfly]"
271 title="Butterfly" src="download/b4.png"></h3>
273 <li><a name="bibtex"></a>A
274 BibTeX database of λδ documentation: <a
275 href="download/lambda_delta.bib"><span
276 style="font-style: italic;">lambda_delta.bib</span></a>,
277 <a style="font-style: italic;"
278 href="download/lambda_delta.txt">lambda_delta.txt</a>
279 (revised <span style="font-weight: bold;">2011-09</span>).</li>
282 <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
284 editing ".hln" files (containing λδ textual syntax): <a
285 style="font-style: italic;"
286 href="download/helena.sl">helena.sl</a>
287 (revised <span style="font-weight: bold;">2010-11</span>).</li>
290 <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
292 editing ".aut" files (containing <a
293 href="http://www.win.tue.nl/automath/">Automath</a>
294 textual syntax): <a style="font-style: italic;"
295 href="download/automath.sl">automath.sl</a>
296 (revised <span style="font-weight: bold;">2008-07</span>).</li>
299 <li>A logo for "basic" λδ: <a href="download/bld.pdf"><span
300 style="font-style: italic;">bld.pdf</span></a>
301 (revised <span style="font-weight: bold;">2008-07</span>).<br>
309 <a href="http://validator.w3.org/check?uri=referer"><img
310 alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
311 Transitional" src="http://www.w3.org/Icons/valid-html401"
312 style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
313 href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
314 Browser Here]" title="Use Any Browser Here"
315 src="download/globe_trans.png" style="border: 0px solid ;
316 width: 147px; height: 42px;"></a> <img style="width: 88px;
317 height: 31px;" alt="[PNG Used Here]" title="PNG Used Here"
318 src="download/PNGnow2.png"><br>
320 Last update 2012-04-16 by <a
321 href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio