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