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