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