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