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 white">
  40               <a href="http://lambdadelta.info/specification.html">specification</a>
  41             </td>
  42             <td class="snnn capitalize italic white">
  43               <br />
  44             </td>
  45             <td class="snnn capitalize italic white">
  46               <br />
  47             </td>
  48             <td class="snns capitalize italic orange">
  49               <a href="http://lambdadelta.info/documentation.html">documentation</a>
  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 white">
  66               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
  67             </td>
  68             <td class="snnn capitalize white">(<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="snnn capitalize white">
  70               <br />
  71             </td>
  72             <td class="snns capitalize orange">
  73               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
  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 white">
  88               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
  89             </td>
  90             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
  91             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
  92             <td class="snss capitalize orange">
  93               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
  94             </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 (2015-02).</span>
 153       Uses λδ "Version 3" with layer variables as core language.
 154       Supports exportation to Gallina
 155       (the specification language of <a href="http://coq.inria.fr/">Coq</a>),
 156       and to Grafite
 157       (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
 158       The overall validation speed of the "Grundlagen der Analysis"
 159       increases of 34% with respect to version 0.8.1.
 160       <a href="http://lambdadelta.info/documentation.html#ldJ3a">Documentation (J3a)</a>.
 161       [Svn revision: 13035] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>).
 162       <ul>
 163           <li>
 164          The specification of Landau's "Grundlagen der Analysis"
 165          for <a href="http://coq.inria.fr/">Coq 8</a>:
 166          <a href="http://lambdadelta.info/download/grundlagen_2.v">grundlagen_2.v</a>
 167          (revised <span class="emph gamma">2015-02</span>).
 168       </li>
 169           <li>
 170          The specification of Landau's "Grundlagen der Analysis"
 171          for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
 172          <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
 173          (revised <span class="emph gamma">2015-02</span>).
 174       </li>
 175           <li>
 176          The corrected specification of Landau's "Grundlagen der Analysis":
 177          <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
 178          (revised <span class="emph gamma">2014-12</span>).
 179       </li>
 180           <li>
 181             <span class="emph gamma">2015-02.</span>
 182          The translated specification of Landau's "Grundlagen der Analysis"
 183          is successfully validated in λC by <a href="http://coq.inria.fr/">Coq 8.4.3</a>.
 184       </li>
 185           <li>
 186             <span class="emph gamma">2014-12.</span>
 187          The corrected specification of Landau's "Grundlagen der Analysis"
 188          is successfully validated in λδ "Version 3".
 189       </li>
 190         </ul>
 191       </li>
 192     </ul>
 193     <ul xmlns:ld="http://lambdadelta.info/" id="v1">
 194       <li>
 195         <span class="emph beta">Version 0.8.1 (2010-11).</span>
 196       Uses a subset of λδ "Version 4" as intermediate language.
 197       Features importation from ".hln" files containing λδ textual syntax.
 198       The overall validation speed of the "Grundlagen der Analysis"
 199       increases of 22% with respect to version 0.8.0.
 200       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>).
 201       <ul>
 202           <li>
 203          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 204          for editing ".hln" files (containing λδ textual syntax):
 205          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
 206          (revised <span class="emph alpha">2010-11</span>).
 207       </li>
 208           <li>
 209             <span class="emph beta">2009-12.</span>
 210          Helena appears in F. Wiedijk's
 211          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
 212             index of computer math systems</a>.
 213       </li>
 214         </ul>
 215       </li>
 216     </ul>
 217     <ul xmlns:ld="http://lambdadelta.info/" id="v0">
 218       <li>
 219         <span class="emph beta">Version 0.8.0 (2009-09).</span>
 220       Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
 221       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
 222       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
 223       <a href="http://lambdadelta.info/documentation.html#ldR2a">Documentation (R2a)</a>.
 224       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
 225       <ul>
 226           <li>
 227          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
 228          for editing ".aut" files
 229          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
 230          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
 231          (revised <span class="emph gamma">2008-07</span>).
 232       </li>
 233           <li>
 234             <span class="emph beta">2009-09.</span>
 235          Jutting's specification of Landau's "Grundlagen der Analysis"
 236          enters λδ Digital Library.
 237       </li>
 238           <li>
 239             <span class="emph beta">2009-06.</span>
 240          Jutting's specification of Landau's "Grundlagen der Analysis"
 241          is successfully processed, enabling sort inclusion.
 242       </li>
 243         </ul>
 244       </li>
 245     </ul>
 246     <div class="spacer">
 247       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 248     </div>
 249     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 250       <br />
 251     </div>
 252     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 253       <a href="http://validator.w3.org/check?uri=referer">
 254         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 255       </a>
 256       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 257         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 258       </a>
 259       <a href="http://www.w3.org/XML/">
 260         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 261       </a>
 262       <a href="http://www.w3.org/Graphics/PNG/">
 263         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 264       </a>
 265       <a href="http://www.anybrowser.org/campaign/">
 266         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 267       </a>
 268     </div>
 269     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 270       <br />
 271     </div>
 272     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 07 Aug 2015 14:21:47 +0200</div>
 273   </body>
 274 </html>