helm/www/lambdadelta/documentation.html

   1 <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
   2 <html dir="ltr" lang="en-us"><head>
   3
   4
   5
   6     <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
   7
   8     <meta content="Ferruccio Guidi" name="author">
   9     <meta content="The formal system λδ" name="description">
  10     <link rel="shortcut icon" href="images/crux_16.ico"></head><body>
  11     <div style="text-align: center;">
  12       <br>
  13       <a href="http://lambdadelta.info/"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
  14       <h1>The Formal System λδ (\lambda\delta)<br>
  15       </h1>
  16       <h2>Towards the unification of terms, types, environments and
  17         contexts</h2>
  18       <img style="width: 95%; height: 4px;" alt="[Separator]" title="Separator" src="images/rainbow.png"><br>
  19       <table style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
  20         <tbody>
  21           <tr>
  22             <td style="vertical-align: top;">
  23               <ul>
  24                 <li><a href="index.html">Foreword</a></li>
  25               </ul>
  26               <ul>
  27                 <li><a href="news.html">News</a></li>
  28               </ul>
  29               <ul>
  30                 <li>Papers</li>
  31               </ul>
  32               <ul>
  33                 <li><a href="implementation.html">Resources</a><br>
  34                 </li>
  35               </ul>
  36             </td>
  37             <td style="vertical-align: top; text-align: left;">
  38               <h3 style="text-align: right;">Documentation <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b5.png"></h3>
  39               Currently the <span style="font-weight: bold;">main
  40                 source of
  41                 information</span> on λδ (version 1) is <span style="font-weight: bold;">Resource
  42                 1.9</span> below.<br>
  43               A <span style="font-weight: bold;">summary</span> of
  44               basic λδ (version
  45               1) is found in <span style="font-weight: bold;">Resource
  46                 1.5</span>
  47               below.<br>
  48               <h3><img style="width: 32px; height: 32px;" alt="[Basic
  49                   lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 2 (in
  50                 progress):</h3>
  51               <table style="text-align: left; width: 100%;" border="0" cellpadding="2" cellspacing="2">
  52                 <tbody>
  53                   <tr>
  54                     <td style="vertical-align: top;">2.4.<br>
  55                     </td>
  56                     <td style="vertical-align: top;"><a name="ldp7"></a>F.
  57                       Guidi: <a href="download/cie_2010.pdf"><span style="font-style: italic;">An
  58                           Efficient
  59                           Validation Procedure for the Formal System </span><span style="font-style: italic;">λδ</span></a><span style="font-style: italic;"></span>
  60                       (<span style="font-weight: bold;">2010-07</span>).
  61                       In <span style="font-style: italic;">CiE 2010
  62                         Local Proceedings</span>.
  63                       University of Azores, CMATI Booklet, pp. 204-213.
  64                       <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
  65                       <br>
  66                     </td>
  67                   </tr>
  68                   <tr>
  69                     <td style="vertical-align: top;">2.3.<br>
  70                     </td>
  71                     <td style="vertical-align: top;"> <a name="ldp6"></a>F.
  72 Guidi:
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84                       <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2009-16"><span style="font-style: italic;">Landau's
  85                           "Grundlagen der Analysis" from Automath to
  86                           lambda-delta</span></a> (<span style="font-weight: bold;">2009-09)</span>.
  87                       University of
  88                       Bologna, technical report UBLCS-2009-16. <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
  89                       <br>
  90                     </td>
  91                   </tr>
  92                   <tr>
  93                     <td style="vertical-align: top;">2.2.<br>
  94                     </td>
  95                     <td style="vertical-align: top;"><a name="ldt7"></a>F.
  96                       Guidi: <a href="download/ld_talk_7s.pdf"><span style="font-style: italic;">An
  97                           Efficient
  98                           Validation Procedure for the Formal System λδ</span></a>
  99                       (<span style="font-weight: bold;">2010-07</span>).
 100                       Presentation
 101                       at
 102                       CiE
 103                       2010
 104                       (slides).<br>
 105                       <br>
 106                     </td>
 107                   </tr>
 108                   <tr>
 109                     <td style="vertical-align: top;">2.1.<br>
 110                     </td>
 111                     <td style="vertical-align: top;"><a name="ldt6"></a>F.
 112                       Guidi: <a href="download/ld_talk_6s.pdf"><span style="font-style: italic;">A
 113                           Validator
 114                           for the Formal System λδ</span></a> (revised <span style="font-weight: bold;">2010-02</span>).
 115                       Presentation
 116                       at
 117                       the
 118                       University
 119                       of
 120                       Bologna
 121                       (slides). </td>
 122                   </tr>
 123                 </tbody>
 124               </table>
 125               <h3><img style="width: 32px; height: 32px;" alt="[Basic
 126                   lambdadelta Logo]" title="Basic lambdadelta" src="images/basic_32.png"> Basic λδ version 1
 127                 (dismissed):</h3>
 128               <table style="text-align: left; width: 100%;" border="0" cellpadding="2" cellspacing="2">
 129                 <tbody>
 130                   <tr>
 131                     <td style="vertical-align: top;">1.9.<br>
 132                     </td>
 133                     <td style="vertical-align: top;"><a name="ldp5"></a>F.
 134 Guidi:
 135                       <a href="http://doi.acm.org/10.1145/1614431.1614436"><span style="font-style: italic;">The Formal System
 136                           λδ</span></a> (<span style="font-weight: bold;">2009-10</span>). In ACM ToCL 11(1),
 137                       Article
 138                       No. 5 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
 139                       <span style="font-weight: bold;">2008-07</span>).
 140                       CoRR
 141                       identifier <a href="http://arxiv.org/abs/cs/0611040"><span style="font-style: italic;"></span>cs/0611040</a>
 142                       [v10] (revised <span style="font-weight: bold;">2008-09</span>).
 143                       <a href="implementation.html#bibtex">BibTeX
 144                         entry</a>.<br>
 145                       <br>
 146                     </td>
 147                   </tr>
 148                   <tr>
 149                     <td style="vertical-align: top;">1.8.<br>
 150                     </td>
 151                     <td style="vertical-align: top;"><a name="ldp4"></a>F.
 152                       Guidi: <a href="download/cie_2007.pdf"><span style="font-style: italic;">Lambda
 153                           Types on the Lambda Calculus with
 154                           Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
 155                       In <span style="font-style: italic;">CiE 2007
 156                         Local Proceedings</span>.
 157                       University
 158                       of
 159                       Siena,
 160                       technical
 161                       report
 162                       487,
 163                       p.
 164                       387
 165                       (abstract
 166                       of
 167                       a
 168                       presentation). <a href="implementation.html#bibtex">BibTeX
 169                         entry</a>.<br>
 170                       <br>
 171                     </td>
 172                   </tr>
 173                   <tr>
 174                     <td style="vertical-align: top;">1.7.<br>
 175                     </td>
 176                     <td style="vertical-align: top;"><a name="ldp3"></a>F.
 177                       Guidi: <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span style="font-style: italic;">Lambda Types on
 178                           the Lambda Calculus with
 179                           Abbreviations</span></a> (<span style="font-weight: bold;">2006-11</span>).
 180                       University
 181                       of
 182                       Bologna,
 183                       technical
 184                       report
 185                       UBLCS-2006-25. <a href="implementation.html#bibtex">BibTeX
 186                         entry</a>.<br>
 187                       <br>
 188                     </td>
 189                   </tr>
 190                   <tr>
 191                     <td style="vertical-align: top;">1.6.<br>
 192                     </td>
 193                     <td style="vertical-align: top;"><a name="ldp2"></a>F.
 194                       Guidi: <a style="font-style: italic;" href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
 195                         Types
 196                         on
 197                         the
 198                         Lambda
 199                         Calculus
 200                         with
 201                         Abbreviations:
 202                         a
 203                         Certified
 204                         Specification</a> (<span style="font-weight: bold;">2006-01</span>).
 205                       University of
 206                       Bologna, technical report UBLCS-2006-01. <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
 207                       <br>
 208                     </td>
 209                   </tr>
 210                   <tr>
 211                     <td style="vertical-align: top;">1.5.<br>
 212                     </td>
 213                     <td style="vertical-align: top;"><a name="ldt5"></a>F.
 214                       Guidi: <a style="font-style: italic;" href="download/ld_talk_5s.pdf">The
 215                         Formal
 216                         System </a><a href="download/cie_2010.pdf"><span style="font-style: italic;">λδ</span></a>
 217                       (<span style="font-weight: bold;">2008-10</span>).
 218                       Presentation at
 219                       "Advances in Constructive Topology and Logical
 220                       Foundations" (slides).<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="ldt4"></a>F.
 228                       Guidi: <a href="download/ld_talk_4s.pdf"><span style="font-style: italic;">Towards
 229                           the Unification of Terms, Types
 230                           and Contexts</span></a> (<span style="font-weight: bold;">2008-03</span>).
 231                       Presentation
 232                       at
 233                       Types
 234                       2008
 235                       (slides).<br>
 236                       <br>
 237                     </td>
 238                   </tr>
 239                   <tr>
 240                     <td style="vertical-align: top;">1.3.<br>
 241                     </td>
 242                     <td style="vertical-align: top;"><a name="ldt3"></a>F.
 243                       Guidi: <a href="download/ld_talk_3s.pdf"><span style="font-style: italic;">Lambda
 244                           Types on the Lambda Calculus with
 245                           Abbreviations</span></a> (<span style="font-weight: bold;">2007-06</span>).
 246                       Presentation
 247                       at
 248                       CiE
 249                       2007
 250                       (slides).<br>
 251                       <br>
 252                     </td>
 253                   </tr>
 254                   <tr>
 255                     <td style="vertical-align: top;">1.2.<br>
 256                     </td>
 257                     <td style="vertical-align: top;"><a name="ldt2"></a>F.
 258                       Guidi: <a href="download/ld_talk_2s.pdf"><span style="font-style: italic;">Lambda
 259                           Tipi sul Lambda Calcolo con
 260                           Abbreviazioni</span></a> (<span style="font-weight: bold;">2007-01</span>).
 261                       Presentation
 262                       at
 263                       the
 264                       University
 265                       of
 266                       Padova
 267                       (slides <span style="font-weight: bold;">in
 268                         Italian</span>).<br>
 269                       <br>
 270                     </td>
 271                   </tr>
 272                   <tr>
 273                     <td style="vertical-align: top;">1.1.<br>
 274                     </td>
 275                     <td style="vertical-align: top;"><a name="ldt1"></a>F.
 276 Guidi:
 277                       <a href="download/ld_talk_1s.pdf"><span style="font-style: italic;">Lambda Tipi sul
 278                           Lambda Calcolo con
 279                           Abbreviazioni: una Specifica Certificata</span></a>
 280                       (<span style="font-weight: bold;">2005-12</span>).
 281                       Presentation at
 282                       the University of Bologna (slides <span style="font-weight: bold;">in
 283                         Italian</span>).<br>
 284                     </td>
 285                   </tr>
 286                 </tbody>
 287               </table>
 288             </td>
 289           </tr>
 290         </tbody>
 291       </table>
 292       <br>
 293       <a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
 294           Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
 295           Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here]" src="images/PNGnow2.png"><br>
 296       <br>
 297       Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 298         Guidi</a><br>
 299     </div>
 300
 301
 302 </body></html>