]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/documentation.html
56ff9c6fb5ce7dedfa397287b5a162c668174192
[helm.git] / helm / www / lambdadelta / documentation.html
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
2 <html dir="ltr" lang="en-us">
3 <head>
4   <meta content="text/html; charset=UTF-8" http-equiv="content-type">
5   <title>λδ home page</title>
6   <meta content="Ferruccio Guidi" name="author">
7   <meta content="The formal system λδ" name="description">
8   <link rel="shortcut icon" href="images/crux_16.ico">
9 </head>
10 <body>
11 <div style="text-align: center;"> <br>
12 <a href="http://lambdadelta.info/"><img alt="[Crux Logo]"
13  title="The Crux" src="images/crux_32.png"
14  style="border: 0px solid ; width: 32px; height: 32px;"></a>
15 <h1>The Formal System λδ (\lambda\delta)<br>
16 </h1>
17 <h2>Towards the unification of terms, types, environments and contexts</h2>
18 <img style="width: 95%; height: 4px;" alt="[Separator]"
19  title="Separator" src="images/rainbow.png"><br>
20 <table
21  style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;"
22  border="0" cellpadding="2" cellspacing="20">
23   <tbody>
24     <tr>
25       <td style="vertical-align: top;">
26       <ul>
27         <li><a href="index.html">Foreword</a></li>
28       </ul>
29       <ul>
30         <li><a href="news.html">News</a></li>
31       </ul>
32       <ul>
33         <li>Papers</li>
34       </ul>
35       <ul>
36         <li><a href="implementation.html">Resources</a><br>
37         </li>
38       </ul>
39       </td>
40       <td style="vertical-align: top; text-align: left;">
41       <h3 style="text-align: right;">Documentation <img
42  style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
43  src="images/b5.png"></h3>
44       <h3><img style="width: 32px; height: 32px;"
45  alt="[Basic
46                   lambdadelta Logo]"
47  title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version
48 2 (in progress):</h3>
49 The <span style="font-weight: bold;">main source of
50 information</span> is <span style="font-weight: bold;">Resource P8</span>.<br>
51       <br>
52       <table style="text-align: left; width: 100%;" border="0"
53  cellpadding="2" cellspacing="2">
54         <tbody>
55           <tr>
56             <td style="vertical-align: top;">R5.<br>
57             </td>
58             <td style="vertical-align: top;"><a name="ldp7"></a>F.
59 Guidi: <a href="download/cie_2010.pdf"><span
60  style="font-style: italic;">An Efficient Validation Procedure for the
61 Formal System </span><span style="font-style: italic;">λδ</span></a><span
62  style="font-style: italic;"></span> (<span style="font-weight: bold;">2010-07</span>).
63
64 In
65
66             <span style="font-style: italic;">CiE 2010 Local Proceedings</span>.
67
68 University
69 of
70 Azores, CMATI Booklet, pp. 204-213. <a
71  href="implementation.html#bibtex">BibTeX entry</a>.<br>
72             <br>
73             </td>
74           </tr>
75           <tr>
76             <td style="vertical-align: top;">R4.<br>
77             </td>
78             <td style="vertical-align: top;"> <a name="ldp6"></a>F.
79 Guidi: <a
80  href="http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16"><span
81  style="font-style: italic;">Landau's "Grundlagen der Analysis" from
82 Automath to lambda-delta</span></a> (<span style="font-weight: bold;">2009-09)</span>.
83
84 University
85 of
86 Bologna, technical report UBLCS-2009-16. <a
87  href="implementation.html#bibtex">BibTeX entry</a>.<br>
88             <div style="text-align: left;"><br>
89             </div>
90             </td>
91           </tr>
92           <tr>
93             <td style="vertical-align: top;">P8.<br>
94             </td>
95             <td style="vertical-align: top;"><a name="ldt8"></a>F.Guidi:
96             <a style="font-style: italic;"
97  href="download/ld_talk_8s.pdf">The Formal System λδ and the "Three
98 Problems"</a> (<span style="font-weight: bold;">2014-06</span>).
99 Presentation at University of Bologna (slides).<br>
100             <br>
101             </td>
102           </tr>
103           <tr>
104             <td style="vertical-align: top;">P7.<br>
105             </td>
106             <td style="vertical-align: top;"><a name="ldt7"></a>F.
107 Guidi: <a href="download/ld_talk_7s.pdf"><span
108  style="font-style: italic;">An Efficient Validation Procedure for the
109 Formal System λδ</span></a> (<span style="font-weight: bold;">2010-07</span>).
110
111 Presentation
112 at
113 CiE 2010 (slides).<br>
114             <br>
115             </td>
116           </tr>
117           <tr>
118             <td style="vertical-align: top;">P6.<br>
119             </td>
120             <td style="vertical-align: top;"><a name="ldt6"></a>F.
121 Guidi: <a href="download/ld_talk_6s.pdf"><span
122  style="font-style: italic;">A Validator for the Formal System λδ</span></a>
123 (revised <span style="font-weight: bold;">2010-02</span>).
124 Presentation at University of Bologna (slides). </td>
125           </tr>
126         </tbody>
127       </table>
128       <h3><img style="width: 32px; height: 32px;"
129  alt="[Basic
130                   lambdadelta Logo]"
131  title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version
132 1 (dismissed):</h3>
133 The <span style="font-weight: bold;">main source of
134 information</span> is <span style="font-weight: bold;">Resource J1</span>.
135 A <span style="font-weight: bold;">summary</span> is found in <span
136  style="font-weight: bold;">Resource P5</span>.<br>
137       <br>
138       <table style="text-align: left; width: 100%;" border="0"
139  cellpadding="2" cellspacing="2">
140         <tbody>
141           <tr>
142             <td style="vertical-align: top;">J1.<br>
143             </td>
144             <td style="vertical-align: top;"><a name="ldp5"></a>F.
145 Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436"><span
146  style="font-style: italic;">The Formal System λδ</span></a> (<span
147  style="font-weight: bold;">2009-11</span>). In ACM ToCL 11(1), pp.
148 5:1-5:37 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
149             <span style="font-weight: bold;">2008-07</span>). CoRR
150 identifier <a href="http://arxiv.org/abs/cs/0611040"><span
151  style="font-style: italic;"></span>cs/0611040</a> [v10] (revised <span
152  style="font-weight: bold;">2008-09</span>). <a
153  href="implementation.html#bibtex">BibTeX entry</a>.<br>
154             <br>
155             </td>
156           </tr>
157           <tr>
158             <td style="vertical-align: top;">R3.<br>
159             </td>
160             <td style="vertical-align: top;"><a name="ldp4"></a>F.
161 Guidi: <a href="download/cie_2007.pdf"><span
162  style="font-style: italic;">Lambda Types on the Lambda Calculus with
163 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
164
165 In
166
167             <span style="font-style: italic;">CiE 2007 Local Proceedings</span>.
168
169 University
170 of
171 Siena, technical report 487, p. 387 (abstract of a
172 presentation). <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
173             <br>
174             </td>
175           </tr>
176           <tr>
177             <td style="vertical-align: top;">R2.<br>
178             </td>
179             <td style="vertical-align: top;"><a name="ldp3"></a>F.
180 Guidi: <a
181  href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25"><span
182  style="font-style: italic;">Lambda Types on the Lambda Calculus with
183 Abbreviations</span></a> (<span style="font-weight: bold;">2006-11</span>).
184
185 University
186 of
187 Bologna, technical report UBLCS-2006-25. <a
188  href="implementation.html#bibtex">BibTeX entry</a>.<br>
189             <br>
190             </td>
191           </tr>
192           <tr>
193             <td style="vertical-align: top;">R1.<br>
194             </td>
195             <td style="vertical-align: top;"><a name="ldp2"></a>F.
196 Guidi: <a style="font-style: italic;"
197  href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01">Lambda
198
199 Types
200 on
201 the Lambda Calculus with Abbreviations: a Certified
202 Specification</a> (<span style="font-weight: bold;">2006-01</span>).
203 University of Bologna, technical report UBLCS-2006-01. <a
204  href="implementation.html#bibtex">BibTeX entry</a>.<br>
205             <br>
206             </td>
207           </tr>
208           <tr>
209             <td style="vertical-align: top;">P5.<br>
210             </td>
211             <td style="vertical-align: top;"><a name="ldt5"></a>F.
212 Guidi: <a style="font-style: italic;" href="download/ld_talk_5s.pdf">The
213
214 Formal
215 System
216             </a><a href="download/cie_2010.pdf"><span
217  style="font-style: italic;">λδ</span></a> (<span
218  style="font-weight: bold;">2008-10</span>). Presentation at "Advances
219 in Constructive Topology and Logical Foundations" (slides).<br>
220             <br>
221             </td>
222           </tr>
223           <tr>
224             <td style="vertical-align: top;">P4.<br>
225             </td>
226             <td style="vertical-align: top;"><a name="ldt4"></a>F.
227 Guidi: <a href="download/ld_talk_4s.pdf"><span
228  style="font-style: italic;">Towards the Unification of Terms, Types
229 and Contexts</span></a> (<span style="font-weight: bold;">2008-03</span>).
230
231 Presentation
232 at
233 Types 2008 (slides).<br>
234             <br>
235             </td>
236           </tr>
237           <tr>
238             <td style="vertical-align: top;">P3.<br>
239             </td>
240             <td style="vertical-align: top;"><a name="ldt3"></a>F.
241 Guidi: <a href="download/ld_talk_3s.pdf"><span
242  style="font-style: italic;">Lambda Types on the Lambda Calculus with
243 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
244
245 Presentation
246 at
247 CiE 2007 (slides).<br>
248             <br>
249             </td>
250           </tr>
251           <tr>
252             <td style="vertical-align: top;">P2.<br>
253             </td>
254             <td style="vertical-align: top;"><a name="ldt2"></a>F.
255 Guidi: <a href="download/ld_talk_2s.pdf"><span
256  style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
257 Abbreviazioni</span></a> (<span style="font-weight: bold;">2007-01</span>).
258
259 Presentation
260 at
261 University of Padova (slides <span style="font-weight: bold;">in
262 Italian</span>).<br>
263             <br>
264             </td>
265           </tr>
266           <tr>
267             <td style="vertical-align: top;">P1.<br>
268             </td>
269             <td style="vertical-align: top;"><a name="ldt1"></a>F.
270 Guidi: <a href="download/ld_talk_1s.pdf"><span
271  style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
272 Abbreviazioni: una Specifica Certificata</span></a> (<span
273  style="font-weight: bold;">2005-12</span>). Presentation at University
274 of Bologna (slides <span style="font-weight: bold;">in
275 Italian</span>).<br>
276             </td>
277           </tr>
278         </tbody>
279       </table>
280       </td>
281     </tr>
282   </tbody>
283 </table>
284 <br>
285 <a href="http://validator.w3.org/check?uri=referer"><img
286  alt="[Valid HTML 4.01 Transitional]"
287  title="Valid HTML 4.01
288           Transitional"
289  src="http://www.w3.org/Icons/valid-html401"
290  style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
291  href="http://www.anybrowser.org/campaign/"><img
292  alt="[Use Any
293           Browser Here]" title="Use Any Browser Here"
294  src="images/globe_trans.png"
295  style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
296  style="width: 88px; height: 31px;" alt="[PNG Used Here]"
297  title="PNG Used Here]" src="images/PNGnow2.png"><br>
298 <br>
299 Last update 2014-06-19 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
300 Guidi</a><br>
301 </div>
302 </body>
303 </html>