helm/www/lambdadelta/index.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>lambdadelta home page</title>
   6   <meta content="Ferruccio Guidi" name="author">
   7   <meta content="The formal system lambdadelta" 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://lambdadelta.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 λδ (lambdadelta)<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>Foreword</li>
  29       </ul>
  30       <ul>
  31         <li><a href="news.html">News</a></li>
  32       </ul>
  33       <ul>
  34         <li><a href="documentation.html">Papers</a></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;">Foreword <img
  43  style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
  44  src="download/b9.png"></h3>
  45 The formal system λδ
  46 (lambdadelta) is a typed lambda calculus that pursues the static and
  47 dynamic unification of terms, types, environments and contexts while
  48 enjoying a well-conceived meta-theory, which includes the commonly
  49 desired properties.<br>
  50       <br>
  51 λδ takes some features from the calculi of the Automath family and
  52 some from the pure type systems, but it differs from both in that it
  53 does not include the Π construction while it provides for an
  54 abbreviation mechanism at the level of terms.<br>
  55       <br>
  56 λδ features explicit type annotations, which are borrowed from
  57 realistic type checker implementations and with which type checking is
  58 reduced to type inference.<br>
  59       <br>
  60 The reduction steps of λδ include β-contraction, δ-expansion,
  61 ζ-contraction and θ-swap. On the other hand,
  62 η-contraction is not included.<br>
  63       <br>
  64 The meta-theory of λδ includes important properties such as the
  65 confluence of reduction, the correctness of types, the
  66 uniqueness of types up to conversion, the subject reduction of the type
  67 assignment, the strong normalization of the typed terms. The
  68 decidability of type inference and of type checking come as corollaries.<br>
  69       <br>
  70 λδ features uniformly dependent types and a predicative abstraction
  71 mechanism, so the calculus can serve as a formal specification language
  72 for the type theories that need a predicative foundation. λδ is
  73 expected to have the expressive power of λ→.<br>
  74       <br>
  75 λδ comes in several versions listed in the following table, which
  76 includes the major milestones:<br>
  77       <br>
  78       <table style="text-align: left; width: 100%;" border="1"
  79  cellpadding="2" cellspacing="0">
  80         <tbody>
  81           <tr>
  82             <td
  83  style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Version<br>
  84             </td>
  85             <td
  86  style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Name<br>
  87             </td>
  88             <td
  89  style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Started<br>
  90             </td>
  91             <td
  92  style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Released<br>
  93             </td>
  94             <td
  95  style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Dismissed<br>
  96             </td>
  97           </tr>
  98           <tr>
  99             <td
 100  style="vertical-align: top; background-color: rgb(255, 223, 191);">2<br>
 101             </td>
 102             <td
 103  style="vertical-align: top; background-color: rgb(255, 223, 191);">basic_2<br>
 104             </td>
 105             <td
 106  style="vertical-align: top; background-color: rgb(255, 223, 191);">April
 107 2011<br>
 108             </td>
 109             <td
 110  style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
 111 in
 112 2013<br>
 113             </td>
 114             <td
 115  style="vertical-align: top; background-color: rgb(255, 223, 191);">not
 116 planned yet<br>
 117             </td>
 118           </tr>
 119           <tr>
 120             <td
 121  style="vertical-align: top; background-color: rgb(255, 191, 191);">1<br>
 122             </td>
 123             <td
 124  style="vertical-align: top; background-color: rgb(255, 191, 191);">basic_1<br>
 125             </td>
 126             <td
 127  style="vertical-align: top; background-color: rgb(255, 191, 191);">May
 128 2004<br>
 129             </td>
 130             <td
 131  style="vertical-align: top; background-color: rgb(255, 191, 191);">November
 132 2006<br>
 133             </td>
 134             <td
 135  style="vertical-align: top; background-color: rgb(255, 191, 191);">May
 136 2008<br>
 137             </td>
 138           </tr>
 139         </tbody>
 140       </table>
 141       <br>
 142       <h3 style="text-align: right;">Notice
 143 for
 144 the
 145 Internet
 146 Explorer
 147 user <img style="width: 37px; height: 37px;" alt="[Butterfly]"
 148  title="Butterfly" src="download/b3.png"></h3>
 149 To view this site
 150 correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a>
 151 support.
 152 For example <span style="font-weight: bold;">Lucida Sans Unicode</span>
 153 (it should be already installed on your system).
 154 To change the current font follow: <span style="font-weight: bold;">"Tools"
 155 menu
 156 → "Internet
 157 Options" entry → "General" tab → "Fonts" button.</span><br>
 158       </td>
 159     </tr>
 160   </tbody>
 161 </table>
 162 <br>
 163 <a href="http://validator.w3.org/check?uri=referer"><img
 164  alt="[Valid HTML 4.01 Transitional]"
 165  title="Valid HTML 4.01 Transitional"
 166  src="http://www.w3.org/Icons/valid-html401"
 167  style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
 168  href="http://www.anybrowser.org/campaign/"><img
 169  alt="[Use Any Browser Here]" title="Use Any Browser Here"
 170  src="download/globe_trans.png"
 171  style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
 172  style="width: 88px; height: 31px;" alt="[PNG Used Here]"
 173  title="PNG Used Here" src="download/PNGnow2.png"><br>
 174 <br>
 175 Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 176 Guidi</a><br>
 177 </div>
 178 </body>
 179 </html>