]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambda_delta/documentation.html
additions to Basic_2
[helm.git] / helm / www / lambda_delta / documentation.html
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
2 <html>
3 <head>
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">
9 </head>
10 <body>
11 <div style="text-align: center;">
12 <br>
13 <a href="http://lambda-delta.info"><img alt="[Crux Logo]"
14  title="The Crux" src="download/crux_32.png"
15  style="border: 0px solid ; width: 32px; height: 32px;"></a>
16 <h1>The Formal System λδ (lambda_delta)<br>
17 </h1>
18 <h2>Towards the unification of terms, types, environments and contexts</h2>
19 <img style="width: 95%; height: 4px;" alt="[Separator]"
20  title="Separator" src="download/rainbow.png"><br>
21 <table
22  style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;"
23  border="0" cellpadding="2" cellspacing="20">
24   <tbody>
25     <tr>
26       <td style="vertical-align: top;">
27       <ul>
28         <li><a href="index.html">Foreword</a></li>
29       </ul>
30       <ul>
31         <li><a href="news.html">News</a></li>
32       </ul>
33       <ul>
34         <li>Papers</li>
35       </ul>
36       <ul>
37         <li><a href="implementation.html">Resources</a><br>
38         </li>
39       </ul>
40       </td>
41       <td style="vertical-align: top; text-align: left;">
42       <h3 style="text-align: right;">Documentation <img
43  style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
44  src="download/b5.png"></h3>
45 Currently the <span style="font-weight: bold;">main source of
46 information</span> on λδ (version 1) is <span
47  style="font-weight: bold;">Resource
48 1.1</span> below.<br>
49 A <span style="font-weight: bold;">summary</span> of basic λδ (version
50 1) is found in <span style="font-weight: bold;">Resource 1.5</span>
51 below.<br>
52       <h3><img style="width: 32px; height: 32px;"
53  alt="[Basic lambda_delta Logo]" title="Basic lambda_delta"
54  src="download/basic_32.png"> Basic λδ version 2:</h3>
55       <table style="text-align: left; width: 100%;" border="0"
56  cellpadding="2" cellspacing="2">
57         <tbody>
58           <tr>
59             <td style="vertical-align: top;">2.1.<br>
60             </td>
61             <td style="vertical-align: top;">F. Guidi: <a
62  href="download/cie_2010.pdf"><span style="font-style: italic;">An
63 Efficient
64 Validation Procedure for the Formal System </span><span
65  style="font-style: italic;">λδ</span></a><span
66  style="font-style: italic;"></span>
67 (<span style="font-weight: bold;">2010-07</span>). In <span
68  style="font-style: italic;">CiE 2010 Local Proceedings</span>.
69 University of Azores, CMATI Booklet, pp. 204-213. <a
70  href="implementation.html#bibtex">BibTeX entry</a>.<br>
71             <br>
72             </td>
73           </tr>
74           <tr>
75             <td style="vertical-align: top;">2.2.<br>
76             </td>
77             <td style="vertical-align: top;"> <a name="ublcs-2009-16"></a>F.
78 Guidi:
79
80
81
82
83
84
85
86
87
88             <a
89  href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2009-16"><span
90  style="font-style: italic;">Landau's
91 "Grundlagen der Analysis" from Automath to lambda-delta</span></a> (<span
92  style="font-weight: bold;">2009-09)</span>. University of
93 Bologna, technical report UBLCS-2009-16. <a
94  href="implementation.html#bibtex">BibTeX entry</a>.<br>
95             <br>
96             </td>
97           </tr>
98           <tr>
99             <td style="vertical-align: top;">2.3.<br>
100             </td>
101             <td style="vertical-align: top;">F. Guidi: <a
102  href="download/ld_talk_7s.pdf"><span style="font-style: italic;">An
103 Efficient
104 Validation Procedure for the Formal System λδ</span></a> (<span
105  style="font-weight: bold;">2010-07</span>). Presentation
106 at
107 CiE
108 2010
109 (slides).<br>
110             <br>
111             </td>
112           </tr>
113           <tr>
114             <td style="vertical-align: top;">2.4.<br>
115             </td>
116             <td style="vertical-align: top;">F. Guidi: <a
117  href="download/ld_talk_6s.pdf"><span style="font-style: italic;">A
118 Validator
119 for the Formal System λδ</span></a> (revised <span
120  style="font-weight: bold;">2010-02</span>). Presentation
121 at
122 the
123 University
124 of
125 Bologna
126 (slides). </td>
127           </tr>
128         </tbody>
129       </table>
130       <h3><img style="width: 32px; height: 32px;"
131  alt="[Basic lambda_delta Logo]" title="Basic lambda_delta"
132  src="download/basic_32.png"> Basic λδ version 1:</h3>
133       <table style="text-align: left; width: 100%;" border="0"
134  cellpadding="2" cellspacing="2">
135         <tbody>
136           <tr>
137             <td style="vertical-align: top;">1.1.<br>
138             </td>
139             <td style="vertical-align: top;"><a name="tocl1"></a>F.
140 Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436"><span
141  style="font-style: italic;">The Formal System λδ</span></a> (<span
142  style="font-weight: bold;">2009-10</span>). In ACM ToCL 11(1), Article
143 No. 5 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
144             <span style="font-weight: bold;">2008-07</span>). CoRR
145 identifier <a href="http://arxiv.org/abs/cs/0611040"><span
146  style="font-style: italic;"></span>cs/0611040</a> [v10] (revised <span
147  style="font-weight: bold;">2008-09</span>). <a
148  href="implementation.html#bibtex">BibTeX
149 entry</a>.<br>
150             <br>
151             </td>
152           </tr>
153           <tr>
154             <td style="vertical-align: top;">1.2.<br>
155             </td>
156             <td style="vertical-align: top;">F. Guidi: <a
157  href="download/cie_2007.pdf"><span
158  style="font-style: italic;">Lambda Types on the Lambda Calculus with
159 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
160 In
161
162
163
164
165
166
167
168
169
170
171
172
173
174             <span style="font-style: italic;">CiE 2007 Local Proceedings</span>.
175 University
176 of
177 Siena,
178 technical
179 report
180 487,
181 p.
182 387
183 (abstract
184 of
185 a
186 presentation).
187
188
189
190
191
192
193
194             <a href="implementation.html#bibtex">BibTeX
195 entry</a>.<br>
196             <br>
197             </td>
198           </tr>
199           <tr>
200             <td style="vertical-align: top;">1.3.<br>
201             </td>
202             <td style="vertical-align: top;">F. Guidi: <a
203  href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span
204  style="font-style: italic;">Lambda Types on the Lambda Calculus with
205 Abbreviations</span></a> (<span style="font-weight: bold;">2006-11</span>).
206 University
207 of
208 Bologna,
209 technical
210 report
211 UBLCS-2006-25.
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226             <a href="implementation.html#bibtex">BibTeX
227 entry</a>.<br>
228             <br>
229             </td>
230           </tr>
231           <tr>
232             <td style="vertical-align: top;">1.4.<br>
233             </td>
234             <td style="vertical-align: top;">F. Guidi: <a
235  style="font-style: italic;"
236  href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
237 Types
238 on
239 the
240 Lambda
241 Calculus
242 with
243 Abbreviations:
244 a
245 Certified
246 Specification</a> (<span style="font-weight: bold;">2006-01</span>).
247 University of
248 Bologna, technical report UBLCS-2006-01. <a
249  href="implementation.html#bibtex">BibTeX entry</a>.<br>
250             <br>
251             </td>
252           </tr>
253           <tr>
254             <td style="vertical-align: top;">1.5.<br>
255             </td>
256             <td style="vertical-align: top;">F. Guidi: <a
257  style="font-style: italic;" href="download/ld_talk_5s.pdf">The
258 Formal
259 System lambda-delta</a>
260 (<span style="font-weight: bold;">2008-10</span>). Presentation at
261 "Advances in Constructive Topology and Logical Foundations" (slides).<br>
262             <br>
263             </td>
264           </tr>
265           <tr>
266             <td style="vertical-align: top;">1.6.<br>
267             </td>
268             <td style="vertical-align: top;">F. Guidi: <a
269  href="download/ld_talk_4s.pdf"><span
270  style="font-style: italic;">Towards the Unification of Terms, Types
271 and Contexts</span></a> (<span style="font-weight: bold;">2008-03</span>).
272 Presentation
273 at
274 Types
275 2008
276 (slides).<br>
277             <br>
278             </td>
279           </tr>
280           <tr>
281             <td style="vertical-align: top;">1.7.<br>
282             </td>
283             <td style="vertical-align: top;">F. Guidi: <a
284  href="download/ld_talk_3s.pdf"><span
285  style="font-style: italic;">Lambda Types on the Lambda Calculus with
286 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
287 Presentation
288 at
289 CiE
290 2007
291 (slides).<br>
292             <br>
293             </td>
294           </tr>
295           <tr>
296             <td style="vertical-align: top;">1.8.<br>
297             </td>
298             <td style="vertical-align: top;">F. Guidi: <a
299  href="download/ld_talk_2s.pdf"><span
300  style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
301 Abbreviazioni</span></a> (<span style="font-weight: bold;">2007-01</span>).
302 Presentation
303 at
304 the
305 University
306 of
307 Padova
308 (slides
309
310
311
312
313
314
315
316             <span style="font-weight: bold;">in
317 Italian</span>).<br>
318             <br>
319             </td>
320           </tr>
321           <tr>
322             <td style="vertical-align: top;">1.9.<br>
323             </td>
324             <td style="vertical-align: top;"><a name="bologna1"></a>F.
325 Guidi: <a
326  href="download/ld_talk_1s.pdf"><span
327  style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
328 Abbreviazioni: una Specifica Certificata</span></a> (<span
329  style="font-weight: bold;">2005-12</span>). Presentation at
330 the University of Bologna (slides <span style="font-weight: bold;">in
331 Italian</span>).<br>
332             </td>
333           </tr>
334         </tbody>
335       </table>
336       </td>
337     </tr>
338   </tbody>
339 </table>
340 <br>
341 <a href="http://validator.w3.org/check?uri=referer"><img
342  alt="[Valid HTML 4.01 Transitional]"
343  title="Valid HTML 4.01 Transitional"
344  src="http://www.w3.org/Icons/valid-html401"
345  style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
346  href="http://www.anybrowser.org/campaign/"><img
347  alt="[Use Any Browser Here]" title="Use Any Browser Here"
348  src="download/globe_trans.png"
349  style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
350  style="width: 88px; height: 31px;" alt="[PNG Used Here]"
351  title="PNG Used Here]"
352  src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png"><br>
353 <br>
354 Last update 2011-09-09 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
355 Guidi</a><br>
356 </div>
357 </body>
358 </html>