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="snns capitalize italic green">
  49               <a href="http://lambdadelta.info/implementation.html">implementation</a>
  50             </td>
  51             <td class="ssnn capitalize italic green">
  52               <br />
  53             </td>
  54           </tr>
  55           <tr>
  56             <td class="snns capitalize sky">
  57               <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
  58             </td>
  59             <td class="snns capitalize magenta">
  60               <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
  61             </td>
  62             <td class="snns capitalize orange">
  63               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
  64             </td>
  65             <td class="snns capitalize green">
  66               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
  67             </td>
  68             <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>
  69             <td class="snns capitalize green">
  70               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
  71             </td>
  72             <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
  73           </tr>
  74           <tr>
  75             <td class="snss capitalize sky">
  76               <a href="http://lambdadelta.info/index.html#citations">citations</a>
  77             </td>
  78             <td class="snss capitalize magenta">
  79               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
  80             </td>
  81             <td class="snss capitalize orange">
  82               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
  83             </td>
  84             <td class="snss capitalize green">
  85               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
  86             </td>
  87             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
  88             <td class="snss capitalize green">
  89               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
  90             </td>
  91             <td class="sssn capitalize green">
  92               <br />
  93             </td>
  94           </tr>
  95         </tbody>
  96       </table>
  97     </div>
  98     <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" />
  99     </div>
 100     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
 101       <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
 102     <div xmlns:ld="http://lambdadelta.info/" class="text">
 103       The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
 104       and contains resources expressed in λδ.
 105    </div>
 106     <ul xmlns:ld="http://lambdadelta.info/" id="contents">
 107       <li>
 108         <span class="emph alpha">Contents:</span>
 109       Landau's "Grundlagen der Analysis"
 110       (from Jutting's specification in  <a href="http://www.win.tue.nl/automath/">Automath</a>).
 111    </li>
 112     </ul>
 113     <ul xmlns:ld="http://lambdadelta.info/" id="access">
 114       <li>
 115         <span class="emph alpha">Access:</span>
 116         <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph gamma">2015-01</span>),
 117       <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph gamma">2014-12</span>),
 118       <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph gamma">2014-12</span>).
 119    </li>
 120     </ul>
 121     <ul xmlns:ld="http://lambdadelta.info/" id="examples">
 122       <li>
 123         <span class="emph alpha">Examples:</span>
 124         <a href="http://lambdadelta.info/static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
 125          Grundlagen's definition "t234"</a>
 126       in λδ version 4.
 127    </li>
 128     </ul>
 129     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
 130       <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
 131     <div xmlns:ld="http://lambdadelta.info/" class="text">
 132       Helena is a processor for λδ,
 133       implemented in <a href="http://caml.inria.fr/">Caml</a>
 134       as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
 135       meant for testing the stable features of the calculus as well as the unstable ones.
 136    </div>
 137     <div xmlns:ld="http://lambdadelta.info/" class="text">
 138       The processor source code is available in the directory
 139       <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>
 140       of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
 141       The Svn revisions containing the stable versions of Helena are indicated next.
 142    </div>
 143     <ul xmlns:ld="http://lambdadelta.info/" id="v2">
 144       <li>
 145         <span class="emph gamma">Version 0.8.2 (2014-12).</span>
 146       Uses λδ "Version 3" with layer variables as core language.
 147       Supports exportation to Grafite
 148       (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
 149       The overall validation speed of the "Grundlagen der Analysis"
 150       increases of 34% with respect to version 0.8.1.
 151       [Svn revision: 13005] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>)
 152       <ul>
 153           <li>
 154          The specification of Landau's "Grundlagen der Analysis"
 155          for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
 156          <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
 157          (revised <span class="emph gamma">2014-12</span>).
 158       </li>
 159           <li>
 160          The corrected specification of Landau's "Grundlagen der Analysis":
 161          <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
 162          (revised <span class="emph gamma">2014-12</span>).
 163       </li>
 164           <li>
 165             <span class="emph gamma">2014-12.</span>
 166          The corrected specification of Landau's "Grundlagen der Analysis"
 167          is successfully validated in λδ "Version 3".
 168       </li>
 169         </ul>
 170       </li>
 171     </ul>
 172     <ul xmlns:ld="http://lambdadelta.info/" id="v1">
 173       <li>
 174         <span class="emph beta">Version 0.8.1 (2010-11).</span>
 175       Uses a subset of λδ "Version 4" as intermediate language.
 176       Features importation from ".hln" files containing λδ textual syntax.
 177       The overall validation speed of the "Grundlagen der Analysis"
 178       increases of 22% with respect to version 0.8.0.
 179       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
 180       <ul>
 181           <li>
 182          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 183          for editing ".hln" files (containing λδ textual syntax):
 184          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
 185          (revised <span class="emph alpha">2010-11</span>).
 186       </li>
 187           <li>
 188             <span class="emph beta">2009-12.</span>
 189          Helena appears in F. Wiedijk's
 190          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
 191             index of computer math systems</a>.
 192       </li>
 193         </ul>
 194       </li>
 195     </ul>
 196     <ul xmlns:ld="http://lambdadelta.info/" id="v0">
 197       <li>
 198         <span class="emph beta">Version 0.8.0 (2009-09).</span>
 199       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
 200       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
 201       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
 202       <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
 203       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
 204       <ul>
 205           <li>
 206          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 207          for editing ".aut" files
 208          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
 209          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
 210          (revised <span class="emph gamma">2008-07</span>).
 211       </li>
 212           <li>
 213             <span class="emph beta">2009-09.</span>
 214          Jutting's specification of Landau's "Grundlagen der Analysis"
 215          enters λδ Digital Library.
 216       </li>
 217           <li>
 218             <span class="emph beta">2009-06.</span>
 219          Jutting's specification of Landau's "Grundlagen der Analysis"
 220          is successfully processed, enabling sort inclusion.
 221       </li>
 222         </ul>
 223       </li>
 224     </ul>
 225     <div class="spacer">
 226       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 227     </div>
 228     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 229       <br />
 230     </div>
 231     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 232       <a href="http://validator.w3.org/check?uri=referer">
 233         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 234       </a>
 235       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 236         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 237       </a>
 238       <a href="http://www.w3.org/XML/">
 239         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 240       </a>
 241       <a href="http://www.w3.org/Graphics/PNG/">
 242         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 243       </a>
 244       <a href="http://www.anybrowser.org/campaign/">
 245         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 246       </a>
 247     </div>
 248     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 249       <br />
 250     </div>
 251     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:44 +0100</div>
 252   </body>
 253 </html>