helm/www/lambdadelta/implementation.html

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
   3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
   4   <head>
   5     <meta http-equiv="Content-Language" content="en-us" />
   6     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
   7     <meta http-equiv="Content-Style-Type" content="text/css" />
   8     <meta name="author" content="Ferruccio Guidi" />
   9     <meta name="description" content="\lambda\delta home page" />
  10     <title>\lambda\delta home page</title>
  11     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
  12     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
  13     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
  14     <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
  15   </head>
  16   <body lang="en-US">
  17     <div class="spacer">
  18       <a href="http://lambdadelta.info/">
  19         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
  20       </a>
  21     </div>
  22     <div class="head1">The Formal System λδ (\lambda\delta)</div>
  23     <div class="spacer">
  24       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
  25     </div>
  26     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
  27       <br />
  28     </div>
  29     <div xmlns:ld="http://lambdadelta.info/" class="text">
  30       <table cellpadding="4" cellspacing="0">
  31         <tbody>
  32           <tr>
  33             <td class="snns capitalize italic sky">
  34               <a href="http://lambdadelta.info/index.html">home</a>
  35             </td>
  36             <td class="snns capitalize italic magenta">
  37               <a href="http://lambdadelta.info/news.html">news</a>
  38             </td>
  39             <td class="snns capitalize italic orange">
  40               <a href="http://lambdadelta.info/documentation.html">documentation</a>
  41             </td>
  42             <td class="snns capitalize italic green">
  43               <a href="http://lambdadelta.info/specification.html">specification</a>
  44             </td>
  45             <td class="snnn capitalize italic green">
  46               <br />
  47             </td>
  48             <td class="snnn capitalize italic green">
  49               <br />
  50             </td>
  51             <td class="snns capitalize italic green">
  52               <a href="http://lambdadelta.info/implementation.html">implementation</a>
  53             </td>
  54             <td class="ssnn capitalize italic green">
  55               <br />
  56             </td>
  57           </tr>
  58           <tr>
  59             <td class="snns capitalize sky">
  60               <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
  61             </td>
  62             <td class="snns capitalize magenta">
  63               <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
  64             </td>
  65             <td class="snns capitalize orange">
  66               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
  67             </td>
  68             <td class="snns capitalize green">
  69               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
  70             </td>
  71             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
  72             <td class="snnn capitalize green">
  73               <br />
  74             </td>
  75             <td class="snns capitalize green">
  76               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
  77             </td>
  78             <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
  79           </tr>
  80           <tr>
  81             <td class="snss capitalize sky">
  82               <a href="http://lambdadelta.info/index.html#citations">citations</a>
  83             </td>
  84             <td class="snss capitalize magenta">
  85               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
  86             </td>
  87             <td class="snss capitalize orange">
  88               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
  89             </td>
  90             <td class="snss capitalize green">
  91               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
  92             </td>
  93             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
  94             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
  95             <td class="snss capitalize green">
  96               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
  97             </td>
  98             <td class="sssn capitalize green">
  99               <br />
 100             </td>
 101           </tr>
 102         </tbody>
 103       </table>
 104     </div>
 105     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="tools">Tools <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
 106     </div>
 107     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
 108       <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
 109     <div xmlns:ld="http://lambdadelta.info/" class="text">
 110       The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
 111       and contains resources expressed in λδ.
 112    </div>
 113     <ul xmlns:ld="http://lambdadelta.info/" id="contents">
 114       <li>
 115         <span class="emph alpha">Contents:</span>
 116       Landau's "Grundlagen der Analysis"
 117       (from Jutting's specification in  <a href="http://www.win.tue.nl/automath/">Automath</a>).
 118    </li>
 119     </ul>
 120     <ul xmlns:ld="http://lambdadelta.info/" id="access">
 121       <li>
 122         <span class="emph alpha">Access:</span>
 123         <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph gamma">2015-01</span>),
 124       <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph gamma">2014-12</span>),
 125       <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph gamma">2014-12</span>).
 126    </li>
 127     </ul>
 128     <ul xmlns:ld="http://lambdadelta.info/" id="examples">
 129       <li>
 130         <span class="emph alpha">Examples:</span>
 131         <a href="http://lambdadelta.info/static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
 132          Grundlagen's definition "t234"</a>
 133       in λδ version 4.
 134    </li>
 135     </ul>
 136     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
 137       <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
 138     <div xmlns:ld="http://lambdadelta.info/" class="text">
 139       Helena is a processor for λδ,
 140       implemented in <a href="http://caml.inria.fr/">Caml</a>
 141       as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
 142       meant for testing the stable features of the calculus as well as the unstable ones.
 143    </div>
 144     <div xmlns:ld="http://lambdadelta.info/" class="text">
 145       The processor source code is available in the directory
 146       <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</a>
 147       of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
 148       The Svn revisions containing the stable versions of Helena are indicated next.
 149    </div>
 150     <ul xmlns:ld="http://lambdadelta.info/" id="v2">
 151       <li>
 152         <span class="emph gamma">Version 0.8.2 (2014-12).</span>
 153       Uses λδ "Version 3" with layer variables as core language.
 154       Supports exportation to Grafite
 155       (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
 156       The overall validation speed of the "Grundlagen der Analysis"
 157       increases of 34% with respect to version 0.8.1.
 158       [Svn revision: 13005] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>)
 159       <ul>
 160           <li>
 161          The specification of Landau's "Grundlagen der Analysis"
 162          for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
 163          <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
 164          (revised <span class="emph gamma">2014-12</span>).
 165       </li>
 166           <li>
 167          The corrected specification of Landau's "Grundlagen der Analysis":
 168          <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
 169          (revised <span class="emph gamma">2014-12</span>).
 170       </li>
 171           <li>
 172             <span class="emph gamma">2014-12.</span>
 173          The corrected specification of Landau's "Grundlagen der Analysis"
 174          is successfully validated in λδ "Version 3".
 175       </li>
 176         </ul>
 177       </li>
 178     </ul>
 179     <ul xmlns:ld="http://lambdadelta.info/" id="v1">
 180       <li>
 181         <span class="emph beta">Version 0.8.1 (2010-11).</span>
 182       Uses a subset of λδ "Version 4" as intermediate language.
 183       Features importation from ".hln" files containing λδ textual syntax.
 184       The overall validation speed of the "Grundlagen der Analysis"
 185       increases of 22% with respect to version 0.8.0.
 186       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
 187       <ul>
 188           <li>
 189          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 190          for editing ".hln" files (containing λδ textual syntax):
 191          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
 192          (revised <span class="emph alpha">2010-11</span>).
 193       </li>
 194           <li>
 195             <span class="emph beta">2009-12.</span>
 196          Helena appears in F. Wiedijk's
 197          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
 198             index of computer math systems</a>.
 199       </li>
 200         </ul>
 201       </li>
 202     </ul>
 203     <ul xmlns:ld="http://lambdadelta.info/" id="v0">
 204       <li>
 205         <span class="emph beta">Version 0.8.0 (2009-09).</span>
 206       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
 207       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
 208       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
 209       <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
 210       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
 211       <ul>
 212           <li>
 213          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 214          for editing ".aut" files
 215          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
 216          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
 217          (revised <span class="emph gamma">2008-07</span>).
 218       </li>
 219           <li>
 220             <span class="emph beta">2009-09.</span>
 221          Jutting's specification of Landau's "Grundlagen der Analysis"
 222          enters λδ Digital Library.
 223       </li>
 224           <li>
 225             <span class="emph beta">2009-06.</span>
 226          Jutting's specification of Landau's "Grundlagen der Analysis"
 227          is successfully processed, enabling sort inclusion.
 228       </li>
 229         </ul>
 230       </li>
 231     </ul>
 232     <div class="spacer">
 233       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 234     </div>
 235     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 236       <br />
 237     </div>
 238     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 239       <a href="http://validator.w3.org/check?uri=referer">
 240         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 241       </a>
 242       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 243         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 244       </a>
 245       <a href="http://www.w3.org/XML/">
 246         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 247       </a>
 248       <a href="http://www.w3.org/Graphics/PNG/">
 249         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 250       </a>
 251       <a href="http://www.anybrowser.org/campaign/">
 252         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 253       </a>
 254     </div>
 255     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 256       <br />
 257     </div>
 258     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
 259   </body>
 260 </html>