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>