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 beta">2014-12</span>),
 115       <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph beta">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          <span class="emph gamma">2014-12.</span>
 151          The corrected specification of Landau's "Grundlagen der Analysis"
 152          is successfully validated in λδ "Version 3".
 153       </li>
 154         </ul>
 155    </li>
 156     </ul>
 157    <ul xmlns:ld="http://lambdadelta.info/" id="v1">
 158       <li>
 159       <span class="emph beta">Version 0.8.1 (2010-11).</span>
 160       Uses a subset of λδ "Version 4" as the intermediate language.
 161       Features importation from ".hln" files containing λδ textual syntax.
 162       The overall validation speed of the "Grundlagen der Analysis"
 163       increases of 22% with respect to version 0.8.0.
 164       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
 165       <ul>
 166           <li>
 167          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 168          for editing ".hln" files (containing λδ textual syntax):
 169          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
 170          (revised <span class="emph alpha">2010-11</span>).
 171       </li>
 172           <li>
 173          <span class="emph beta">2009-12.</span>
 174          Helena appears in F. Wiedijk's
 175          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
 176             index of computer math systems</a>.
 177       </li>
 178         </ul>
 179    </li>
 180     </ul>
 181    <ul xmlns:ld="http://lambdadelta.info/" id="v0">
 182       <li>
 183       <span class="emph beta">Version 0.8.0 (2009-09).</span>
 184       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
 185       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
 186       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
 187       <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
 188       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
 189       <ul>
 190           <li>
 191          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 192          for editing ".aut" files
 193          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
 194          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
 195          (revised <span class="emph gamma">2008-07</span>).
 196       </li>
 197           <li>
 198          <span class="emph beta">2009-09.</span>
 199          Jutting's specification of Landau's "Grundlagen der Analysis"
 200          enters λδ Digital Library.
 201       </li>
 202           <li>
 203          <span class="emph beta">2009-06.</span>
 204          Jutting's specification of Landau's "Grundlagen der Analysis"
 205          is successfully processed, enabling sort inclusion.
 206       </li>
 207         </ul>
 208    </li>
 209     </ul>
 210    <div class="spacer">
 211       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 212     </div>
 213     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 214       <br />
 215     </div>
 216     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 217       <a href="http://validator.w3.org/check?uri=referer">
 218         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 219       </a>
 220       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 221         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 222       </a>
 223       <a href="http://www.w3.org/XML/">
 224         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 225       </a>
 226       <a href="http://www.w3.org/Graphics/PNG/">
 227         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 228       </a>
 229       <a href="http://www.anybrowser.org/campaign/">
 230         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 231       </a>
 232     </div>
 233     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 234       <br />
 235     </div>
 236     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 23:26:17 +0100</div>
 237 </body>
 238 </html>