helm/www/lambda_delta/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>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"
  15  style="border: 0px 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 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 (lambda-delta) 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       <h3 style="text-align: right;">Notice
  75 for
  76 the
  77 Internet
  78 Explorer
  79 user <img style="width: 37px; height: 37px;" alt="[Butterfly]"
  80  title="Butterfly" src="download/b3.png"></h3>
  81 To view this site
  82 correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a>
  83 support.<br>
  84 For example <span style="font-weight: bold;">Lucida Sans Unicode</span>
  85 (it should be already installed on your system).<br>
  86 To change the current font follow: <br>
  87       <span style="font-weight: bold;">"Tools" menu → "Internet
  88 Options" entry → "General" tab → "Fonts" button.</span><br>
  89       </td>
  90     </tr>
  91   </tbody>
  92 </table>
  93 <br>
  94 <a href="http://validator.w3.org/check?uri=referer"><img
  95  alt="[Valid HTML 4.01 Transitional]"
  96  title="Valid HTML 4.01 Transitional"
  97  src="http://www.w3.org/Icons/valid-html401"
  98  style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
  99  href="http://www.anybrowser.org/campaign/"><img
 100  alt="[Use Any Browser Here]" title="Use Any Browser Here"
 101  src="http://www.cs.unibo.it/%7Efguidi/download/globe-trans.png"
 102  style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
 103  style="width: 88px; height: 31px;" alt="[PNG Used Here]"
 104  title="PNG Used Here"
 105  src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png"><br>
 106 <br>
 107 Last update 2010-12-14 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 108 Guidi</a><br>
 109 </div>
 110 </body>
 111 </html>