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>