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 Currently the <span style="font-weight: bold;">main source of
  45 information</span> on λδ (version 1) is <span
  46  style="font-weight: bold;">Resource J1</span> below.<br>
  47 A <span style="font-weight: bold;">summary</span> of basic λδ (version
  48 1) is found in <span style="font-weight: bold;">Resource P5</span>
  49 below.<br>
  50       <h3><img style="width: 32px; height: 32px;"
  51  alt="[Basic
  52                   lambdadelta Logo]"
  53  title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version
  54 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;">R5.<br>
  60             </td>
  61             <td style="vertical-align: top;"><a name="ldp7"></a>F.
  62 Guidi: <a href="download/cie_2010.pdf"><span
  63  style="font-style: italic;">An Efficient Validation Procedure for the
  64 Formal System </span><span style="font-style: italic;">λδ</span></a><span
  65  style="font-style: italic;"></span> (<span style="font-weight: bold;">2010-07</span>).
  66
  67 In <span style="font-style: italic;">CiE 2010 Local Proceedings</span>.
  68
  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;">R4.<br>
  76             </td>
  77             <td style="vertical-align: top;"> <a name="ldp6"></a>F.
  78 Guidi: <a
  79  href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2009-16"><span
  80  style="font-style: italic;">Landau's "Grundlagen der Analysis" from
  81 Automath to lambda-delta</span></a> (<span style="font-weight: bold;">2009-09)</span>.
  82
  83 University of Bologna, technical report UBLCS-2009-16. <a
  84  href="implementation.html#bibtex">BibTeX entry</a>.<br>
  85             <br>
  86             </td>
  87           </tr>
  88           <tr>
  89             <td style="vertical-align: top;">P7.<br>
  90             </td>
  91             <td style="vertical-align: top;"><a name="ldt7"></a>F.
  92 Guidi: <a href="download/ld_talk_7s.pdf"><span
  93  style="font-style: italic;">An Efficient Validation Procedure for the
  94 Formal System λδ</span></a> (<span style="font-weight: bold;">2010-07</span>).
  95
  96 Presentation at CiE 2010 (slides).<br>
  97             <br>
  98             </td>
  99           </tr>
 100           <tr>
 101             <td style="vertical-align: top;">P6.<br>
 102             </td>
 103             <td style="vertical-align: top;"><a name="ldt6"></a>F.
 104 Guidi: <a href="download/ld_talk_6s.pdf"><span
 105  style="font-style: italic;">A Validator for the Formal System λδ</span></a>
 106 (revised <span style="font-weight: bold;">2010-02</span>).
 107 Presentation at the University of Bologna (slides). </td>
 108           </tr>
 109         </tbody>
 110       </table>
 111       <h3><img style="width: 32px; height: 32px;"
 112  alt="[Basic
 113                   lambdadelta Logo]"
 114  title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version
 115 1 (dismissed):</h3>
 116       <table style="text-align: left; width: 100%;" border="0"
 117  cellpadding="2" cellspacing="2">
 118         <tbody>
 119           <tr>
 120             <td style="vertical-align: top;">J1.<br>
 121             </td>
 122             <td style="vertical-align: top;"><a name="ldp5"></a>F.
 123 Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436"><span
 124  style="font-style: italic;">The Formal System λδ</span></a> (<span
 125  style="font-weight: bold;">2009-11</span>). In ACM ToCL 11(1), pp.
 126 5:1-5:37 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
 127             <span style="font-weight: bold;">2008-07</span>). CoRR
 128 identifier <a href="http://arxiv.org/abs/cs/0611040"><span
 129  style="font-style: italic;"></span>cs/0611040</a> [v10] (revised <span
 130  style="font-weight: bold;">2008-09</span>). <a
 131  href="implementation.html#bibtex">BibTeX entry</a>.<br>
 132             <br>
 133             </td>
 134           </tr>
 135           <tr>
 136             <td style="vertical-align: top;">R3.<br>
 137             </td>
 138             <td style="vertical-align: top;"><a name="ldp4"></a>F.
 139 Guidi: <a href="download/cie_2007.pdf"><span
 140  style="font-style: italic;">Lambda Types on the Lambda Calculus with
 141 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
 142
 143 In <span style="font-style: italic;">CiE 2007 Local Proceedings</span>.
 144
 145 University of Siena, technical report 487, p. 387 (abstract of a
 146 presentation). <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
 147             <br>
 148             </td>
 149           </tr>
 150           <tr>
 151             <td style="vertical-align: top;">R2.<br>
 152             </td>
 153             <td style="vertical-align: top;"><a name="ldp3"></a>F.
 154 Guidi: <a
 155  href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span
 156  style="font-style: italic;">Lambda Types on the Lambda Calculus with
 157 Abbreviations</span></a> (<span style="font-weight: bold;">2006-11</span>).
 158
 159 University of Bologna, technical report UBLCS-2006-25. <a
 160  href="implementation.html#bibtex">BibTeX entry</a>.<br>
 161             <br>
 162             </td>
 163           </tr>
 164           <tr>
 165             <td style="vertical-align: top;">R1.<br>
 166             </td>
 167             <td style="vertical-align: top;"><a name="ldp2"></a>F.
 168 Guidi: <a style="font-style: italic;"
 169  href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
 170
 171 Types on the Lambda Calculus with Abbreviations: a Certified
 172 Specification</a> (<span style="font-weight: bold;">2006-01</span>).
 173 University of Bologna, technical report UBLCS-2006-01. <a
 174  href="implementation.html#bibtex">BibTeX entry</a>.<br>
 175             <br>
 176             </td>
 177           </tr>
 178           <tr>
 179             <td style="vertical-align: top;">P5.<br>
 180             </td>
 181             <td style="vertical-align: top;"><a name="ldt5"></a>F.
 182 Guidi: <a style="font-style: italic;" href="download/ld_talk_5s.pdf">The
 183
 184 Formal System </a><a href="download/cie_2010.pdf"><span
 185  style="font-style: italic;">λδ</span></a> (<span
 186  style="font-weight: bold;">2008-10</span>). Presentation at "Advances
 187 in Constructive Topology and Logical Foundations" (slides).<br>
 188             <br>
 189             </td>
 190           </tr>
 191           <tr>
 192             <td style="vertical-align: top;">P4.<br>
 193             </td>
 194             <td style="vertical-align: top;"><a name="ldt4"></a>F.
 195 Guidi: <a href="download/ld_talk_4s.pdf"><span
 196  style="font-style: italic;">Towards the Unification of Terms, Types
 197 and Contexts</span></a> (<span style="font-weight: bold;">2008-03</span>).
 198
 199 Presentation at Types 2008 (slides).<br>
 200             <br>
 201             </td>
 202           </tr>
 203           <tr>
 204             <td style="vertical-align: top;">P3.<br>
 205             </td>
 206             <td style="vertical-align: top;"><a name="ldt3"></a>F.
 207 Guidi: <a href="download/ld_talk_3s.pdf"><span
 208  style="font-style: italic;">Lambda Types on the Lambda Calculus with
 209 Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
 210
 211 Presentation at CiE 2007 (slides).<br>
 212             <br>
 213             </td>
 214           </tr>
 215           <tr>
 216             <td style="vertical-align: top;">P2.<br>
 217             </td>
 218             <td style="vertical-align: top;"><a name="ldt2"></a>F.
 219 Guidi: <a href="download/ld_talk_2s.pdf"><span
 220  style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
 221 Abbreviazioni</span></a> (<span style="font-weight: bold;">2007-01</span>).
 222
 223 Presentation at the University of Padova (slides <span
 224  style="font-weight: bold;">in Italian</span>).<br>
 225             <br>
 226             </td>
 227           </tr>
 228           <tr>
 229             <td style="vertical-align: top;">P1.<br>
 230             </td>
 231             <td style="vertical-align: top;"><a name="ldt1"></a>F.
 232 Guidi: <a href="download/ld_talk_1s.pdf"><span
 233  style="font-style: italic;">Lambda Tipi sul Lambda Calcolo con
 234 Abbreviazioni: una Specifica Certificata</span></a> (<span
 235  style="font-weight: bold;">2005-12</span>). Presentation at the
 236 University of Bologna (slides <span style="font-weight: bold;">in
 237 Italian</span>).<br>
 238             </td>
 239           </tr>
 240         </tbody>
 241       </table>
 242       </td>
 243     </tr>
 244   </tbody>
 245 </table>
 246 <br>
 247 <a href="http://validator.w3.org/check?uri=referer"><img
 248  alt="[Valid HTML 4.01 Transitional]"
 249  title="Valid HTML 4.01
 250           Transitional"
 251  src="http://www.w3.org/Icons/valid-html401"
 252  style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
 253  href="http://www.anybrowser.org/campaign/"><img
 254  alt="[Use Any
 255           Browser Here]" title="Use Any Browser Here"
 256  src="images/globe_trans.png"
 257  style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
 258  style="width: 88px; height: 31px;" alt="[PNG Used Here]"
 259  title="PNG Used Here]" src="images/PNGnow2.png"><br>
 260 <br>
 261 Last update 2014-02-25 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 262
 263 Guidi</a><br>
 264 </div>
 265 </body>
 266 </html>