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