1 <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
2 <html dir="ltr" lang="en-us"><head>
6 <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
8 <meta content="Ferruccio Guidi" name="author">
9 <meta content="The formal system λδ" name="description">
10 <link rel="shortcut icon" href="images/crux_16.ico"></head><body>
11 <div style="text-align: center;">
13 <a href="http://lambdadelta.info/"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
14 <h1>The Formal System λδ (\lambda\delta)<br>
16 <h2>Towards the unification of terms, types, environments and
18 <img style="width: 95%; height: 4px;" alt="[Separator]" title="Separator" src="images/rainbow.png"><br>
19 <table style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
22 <td style="vertical-align: top;">
24 <li><a href="index.html">Foreword</a></li>
27 <li><a href="news.html">News</a></li>
33 <li><a href="implementation.html">Resources</a><br>
37 <td style="vertical-align: top; text-align: left;">
38 <h3 style="text-align: right;">Documentation <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b5.png"></h3>
39 Currently the <span style="font-weight: bold;">main
41 information</span> on λδ (version 1) is <span style="font-weight: bold;">Resource
43 A <span style="font-weight: bold;">summary</span> of
45 1) is found in <span style="font-weight: bold;">Resource
48 <h3><img style="width: 32px; height: 32px;" alt="[Basic
49 lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 2 (in
51 <table style="text-align: left; width: 100%;" border="0" cellpadding="2" cellspacing="2">
54 <td style="vertical-align: top;">2.4.<br>
56 <td style="vertical-align: top;"><a name="ldp7"></a>F.
57 Guidi: <a href="download/cie_2010.pdf"><span style="font-style: italic;">An
59 Validation Procedure for the Formal System </span><span style="font-style: italic;">λδ</span></a><span style="font-style: italic;"></span>
60 (<span style="font-weight: bold;">2010-07</span>).
61 In <span style="font-style: italic;">CiE 2010
62 Local Proceedings</span>.
63 University of Azores, CMATI Booklet, pp. 204-213.
64 <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
69 <td style="vertical-align: top;">2.3.<br>
71 <td style="vertical-align: top;"> <a name="ldp6"></a>F.
84 <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2009-16"><span style="font-style: italic;">Landau's
85 "Grundlagen der Analysis" from Automath to
86 lambda-delta</span></a> (<span style="font-weight: bold;">2009-09)</span>.
88 Bologna, technical report UBLCS-2009-16. <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
93 <td style="vertical-align: top;">2.2.<br>
95 <td style="vertical-align: top;"><a name="ldt7"></a>F.
96 Guidi: <a href="download/ld_talk_7s.pdf"><span style="font-style: italic;">An
98 Validation Procedure for the Formal System λδ</span></a>
99 (<span style="font-weight: bold;">2010-07</span>).
109 <td style="vertical-align: top;">2.1.<br>
111 <td style="vertical-align: top;"><a name="ldt6"></a>F.
112 Guidi: <a href="download/ld_talk_6s.pdf"><span style="font-style: italic;">A
114 for the Formal System λδ</span></a> (revised <span style="font-weight: bold;">2010-02</span>).
125 <h3><img style="width: 32px; height: 32px;" alt="[Basic
126 lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 1
128 <table style="text-align: left; width: 100%;" border="0" cellpadding="2" cellspacing="2">
131 <td style="vertical-align: top;">1.9.<br>
133 <td style="vertical-align: top;"><a name="ldp5"></a>F.
135 <a href="http://doi.acm.org/10.1145/1614431.1614436"><span style="font-style: italic;">The Formal System
136 λδ</span></a> (<span style="font-weight: bold;">2009-11</span>). In ACM ToCL 11(1),
138 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
139 <span style="font-weight: bold;">2008-07</span>).
141 identifier <a href="http://arxiv.org/abs/cs/0611040"><span style="font-style: italic;"></span>cs/0611040</a>
142 [v10] (revised <span style="font-weight: bold;">2008-09</span>).
143 <a href="implementation.html#bibtex">BibTeX
149 <td style="vertical-align: top;">1.8.<br>
151 <td style="vertical-align: top;"><a name="ldp4"></a>F.
152 Guidi: <a href="download/cie_2007.pdf"><span style="font-style: italic;">Lambda
153 Types on the Lambda Calculus with
154 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
155 In <span style="font-style: italic;">CiE 2007
156 Local Proceedings</span>.
168 presentation). <a href="implementation.html#bibtex">BibTeX
174 <td style="vertical-align: top;">1.7.<br>
176 <td style="vertical-align: top;"><a name="ldp3"></a>F.
177 Guidi: <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span style="font-style: italic;">Lambda Types on
178 the Lambda Calculus with
179 Abbreviations</span></a> (<span style="font-weight: bold;">2006-11</span>).
185 UBLCS-2006-25. <a href="implementation.html#bibtex">BibTeX
191 <td style="vertical-align: top;">1.6.<br>
193 <td style="vertical-align: top;"><a name="ldp2"></a>F.
194 Guidi: <a style="font-style: italic;" href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
204 Specification</a> (<span style="font-weight: bold;">2006-01</span>).
206 Bologna, technical report UBLCS-2006-01. <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
211 <td style="vertical-align: top;">1.5.<br>
213 <td style="vertical-align: top;"><a name="ldt5"></a>F.
214 Guidi: <a style="font-style: italic;" href="download/ld_talk_5s.pdf">The
216 System </a><a href="download/cie_2010.pdf"><span style="font-style: italic;">λδ</span></a>
217 (<span style="font-weight: bold;">2008-10</span>).
219 "Advances in Constructive Topology and Logical
220 Foundations" (slides).<br>
225 <td style="vertical-align: top;">1.4.<br>
227 <td style="vertical-align: top;"><a name="ldt4"></a>F.
228 Guidi: <a href="download/ld_talk_4s.pdf"><span style="font-style: italic;">Towards
229 the Unification of Terms, Types
230 and Contexts</span></a> (<span style="font-weight: bold;">2008-03</span>).
240 <td style="vertical-align: top;">1.3.<br>
242 <td style="vertical-align: top;"><a name="ldt3"></a>F.
243 Guidi: <a href="download/ld_talk_3s.pdf"><span style="font-style: italic;">Lambda
244 Types on the Lambda Calculus with
245 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
255 <td style="vertical-align: top;">1.2.<br>
257 <td style="vertical-align: top;"><a name="ldt2"></a>F.
258 Guidi: <a href="download/ld_talk_2s.pdf"><span style="font-style: italic;">Lambda
259 Tipi sul Lambda Calcolo con
260 Abbreviazioni</span></a> (<span style="font-weight: bold;">2007-01</span>).
267 (slides <span style="font-weight: bold;">in
273 <td style="vertical-align: top;">1.1.<br>
275 <td style="vertical-align: top;"><a name="ldt1"></a>F.
277 <a href="download/ld_talk_1s.pdf"><span style="font-style: italic;">Lambda Tipi sul
279 Abbreviazioni: una Specifica Certificata</span></a>
280 (<span style="font-weight: bold;">2005-12</span>).
282 the University of Bologna (slides <span style="font-weight: bold;">in
293 <a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
294 Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
295 Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here]" src="images/PNGnow2.png"><br>
297 Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio