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