informational page on ground_1

[helm.git] / helm / www / lambdadelta / implementation.html

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 77a7b0f2905e15cf045860416b88a81802f2bb08..82dcacfd5db933f2ca7bbc10168ec928ea5d6ca2 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -23,204 +23,190 @@
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>

-   <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">

       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>

-            <td class="snns component sky">
+            <td class="snns capitalize italic sky">

               <a href="http://lambdadelta.info/index.html">home</a>
             </td>
               <a href="http://lambdadelta.info/index.html">home</a>
             </td>

-            <td class="snns component magenta">
+            <td class="snns capitalize italic magenta">

               <a href="http://lambdadelta.info/news.html">news</a>
             </td>
               <a href="http://lambdadelta.info/news.html">news</a>
             </td>

-            <td class="snns component orange">
+            <td class="snns capitalize italic orange">

               <a href="http://lambdadelta.info/documentation.html">documentation</a>
             </td>
               <a href="http://lambdadelta.info/documentation.html">documentation</a>
             </td>

-            <td class="snns component green">
-              <a href="http://lambdadelta.info/implementation.html">implementation</a>
-            </td>
-            <td class="ssnn component green">(<a href="http://lambdadelta.info/implementation.html#specifications">specifications</a>
-              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
-              <a href="http://lambdadelta.info/implementation.html#helena">Helena</a>)</td>
-          </tr>
-          <tr>
-            <td class="snns sky">
-              <a href="http://lambdadelta.info/index.html#foreword">Foreword</a>
+            <td class="snns capitalize italic green">
+              <a href="http://lambdadelta.info/specification.html">specification</a>

             </td>
             </td>

-            <td class="snns magenta">
-              <a href="http://lambdadelta.info/news.html#milestones">Milestones</a>
+            <td class="snnn capitalize italic green">
+              <br />

             </td>
             </td>

-            <td class="snns orange">
-              <a href="http://lambdadelta.info/documentation.html#v2">Version 2</a>
+            <td class="snnn capitalize italic green">
+              <br />

             </td>
             </td>

-            <td class="snns green">
-              <a href="http://lambdadelta.info/version_2.html">Version 2</a>
+            <td class="snns capitalize italic green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>

             </td>
             </td>

-            <td class="ssnn 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 class="ssnn capitalize italic green">
+              <br />

             </td>
           </tr>
           <tr>
             </td>
           </tr>
           <tr>

-            <td class="snss sky">
-              <a href="http://lambdadelta.info/index.html#notice">Notice</a>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>

             </td>
             </td>

-            <td class="snss magenta">
-              <a href="http://lambdadelta.info/news.html#visibility">Visibility</a>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>

             </td>
             </td>

-            <td class="snss orange">
-              <a href="http://lambdadelta.info/documentation.html#v1">Version 1</a>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>

             </td>
             </td>

-            <td class="snss green">
-              <a href="http://lambdadelta.info/version_1.html">Version 1</a>
+            <td class="snns capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v2">version 2</a>

             </td>
             </td>

-            <td class="sssn green">
+            <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>
+            <td class="snnn capitalize green">

               <br />
             </td>
               <br />
             </td>

-          </tr>
-        </tbody>
-      </table>
-    </div>
-
-   <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
-    </div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      λδ comes in several versions listed in the following table,
-      which includes the major milestones:
-   </div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <table cellpadding="4" cellspacing="0">
-        <tbody>
-          <tr>
-            <td class="snns component gray">version</td>
-            <td class="snnn component gray">name</td>
-            <td class="snnn component gray">developed with</td>
-            <td class="snnn component gray">started</td>
-            <td class="snnn component gray">announced</td>
-            <td class="snnn component gray">released</td>
-            <td class="ssnn component gray">dismissed</td>
+            <td class="snns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+            </td>
+            <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>

           </tr>
           <tr>
           </tr>
           <tr>

-            <td class="snns orange">2</td>
-            <td class="snnn orange">
-              <a href="http://lambdadelta.info/version_2.html">basic_2</a>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#citations">citations</a>

             </td>
             </td>

-            <td class="snnn orange">
-              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>

             </td>
             </td>

-            <td class="snnn orange">April 2011</td>
-            <td class="snnn orange">July 2014</td>
-            <td class="snnn orange">Planned in 2014</td>
-            <td class="ssnn orange">Not planned yet</td>
-          </tr>
-          <tr>
-            <td class="snss red">1</td>
-            <td class="snsn red">
-              <a href="http://lambdadelta.info/version_1.html">basic_1</a>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>

             </td>
             </td>

-            <td class="snsn red">
-              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+            </td>
+            <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>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
+            <td class="sssn capitalize green">
+              <br />

             </td>
             </td>

-            <td class="snsn red">May 2004</td>
-            <td class="snsn red">January 2006</td>
-            <td class="snsn red">November 2006</td>
-            <td class="sssn red">May 2008</td>

           </tr>
         </tbody>
       </table>
     </div>
           </tr>
         </tbody>
       </table>
     </div>

-
-   <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" />
+    <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" />

     </div>
     </div>

-
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="lddl">
+    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">

       <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
       <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>

-   <div xmlns:ld="http://lambdadelta.info/" class="text">
+    <div xmlns:ld="http://lambdadelta.info/" class="text">

       The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
       and contains resources expressed in λδ.      
    </div>
       The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
       and contains resources expressed in λδ.      
    </div>

-   <ul xmlns:ld="http://lambdadelta.info/">
+    <ul xmlns:ld="http://lambdadelta.info/" id="contents">

       <li>
       <li>

-        <span class="date">Contents:</span>
+        <span class="emph alpha">Contents:</span>

       Landau's "Grundlagen der Analysis"
       (from Jutting's specification in  <a href="http://www.win.tue.nl/automath/">Automath</a>).
    </li>
     </ul>
       Landau's "Grundlagen der Analysis"
       (from Jutting's specification in  <a href="http://www.win.tue.nl/automath/">Automath</a>).
    </li>
     </ul>

-   <ul xmlns:ld="http://lambdadelta.info/">
+    <ul xmlns:ld="http://lambdadelta.info/" id="access">

       <li>
       <li>

-        <span class="date">Access:</span>
-      <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="date">2012-10</span>),
-      <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="date">2012-10</span>),
-      <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="date">2012-10</span>).
+        <span class="emph alpha">Access:</span>
+        <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph gamma">2015-01</span>),
+      <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph gamma">2014-12</span>),
+      <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph gamma">2014-12</span>).

    </li>
     </ul>
    </li>
     </ul>

-   <ul xmlns:ld="http://lambdadelta.info/">
+    <ul xmlns:ld="http://lambdadelta.info/" id="examples">

       <li>
       <li>

-        <span class="date">Examples:</span>
-      <a href="http://lambdadelta.info/static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
-         Grundlagen's definition "t234"</a>
-      (in "basic_rg" λδ),
-      <a href="http://lambdadelta.info/static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+        <span class="emph alpha">Examples:</span>
+        <a href="http://lambdadelta.info/static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">

          Grundlagen's definition "t234"</a>
          Grundlagen's definition "t234"</a>

-      (in "complete_rg" λδ).
+      in λδ version 4.

    </li>
     </ul>
    </li>
     </ul>

-
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="helena">
+    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">

       <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
       <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>

-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      Helena is a λδ processor,
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      Helena is a processor for λδ,

       implemented in <a href="http://caml.inria.fr/">Caml</a>
       as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
       meant for testing the stable features of the calculus as well as the unstable ones.
    </div>
       implemented in <a href="http://caml.inria.fr/">Caml</a>
       as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
       meant for testing the stable features of the calculus as well as the unstable ones.
    </div>

-   <div xmlns:ld="http://lambdadelta.info/" class="text">
+    <div xmlns:ld="http://lambdadelta.info/" class="text">

       The processor source code is available in the directory
       <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>
       of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
       The Svn revisions containing the stable versions of Helena are indicated next.
    </div>
       The processor source code is available in the directory
       <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>
       of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
       The Svn revisions containing the stable versions of Helena are indicated next.
    </div>

-   <ul xmlns:ld="http://lambdadelta.info/">
+    <ul xmlns:ld="http://lambdadelta.info/" id="v2">

       <li>
       <li>

-        <span class="date">Version 0.8.2.</span>
-      In progress.
-   </li>
+        <span class="emph gamma">Version 0.8.2 (2014-12).</span>
+      Uses λδ "Version 3" with layer variables as core language.
+      Supports exportation to Grafite
+      (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
+      The overall validation speed of the "Grundlagen der Analysis"
+      increases of 34% with respect to version 0.8.1.
+      [Svn revision: 13005] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>)
+      <ul>
+          <li>
+         The specification of Landau's "Grundlagen der Analysis"
+         for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
+         <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
+         (revised <span class="emph gamma">2014-12</span>).
+      </li>
+          <li>
+         The corrected specification of Landau's "Grundlagen der Analysis":  
+         <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
+         (revised <span class="emph gamma">2014-12</span>).
+      </li>
+          <li>
+            <span class="emph gamma">2014-12.</span>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λδ "Version 3".
+      </li>
+        </ul>
+      </li>

     </ul>
     </ul>

-   <ul xmlns:ld="http://lambdadelta.info/">
+    <ul xmlns:ld="http://lambdadelta.info/" id="v1">

       <li>
       <li>

-        <span class="date">Version 0.8.1 (2010-11).</span>
-      Exploits a subset of "complete_rg" λδ as the intermediate language.
+        <span class="emph beta">Version 0.8.1 (2010-11).</span>
+      Uses a subset of λδ "Version 4" as intermediate language.

       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"

-      increases of 22% with respect toversion 0.8.0.
+      increases of 22% with respect to version 0.8.0.

       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
       <ul>
           <li>
          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
          for editing ".hln" files (containing λδ textual syntax):
          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
       <ul>
           <li>
          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
          for editing ".hln" files (containing λδ textual syntax):
          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>

-         (revised <span class="date">2010-11</span>).
+         (revised <span class="emph alpha">2010-11</span>).

       </li>
           <li>
       </li>
           <li>

-         <span class="date">2009-12.</span>
+            <span class="emph beta">2009-12.</span>

          Helena appears in F. Wiedijk's
          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
             index of computer math systems</a>.
       </li>
         </ul>
          Helena appears in F. Wiedijk's
          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
             index of computer math systems</a>.
       </li>
         </ul>

-   </li>
+      </li>

     </ul>
     </ul>

-   <ul xmlns:ld="http://lambdadelta.info/">
+    <ul xmlns:ld="http://lambdadelta.info/" id="v0">

       <li>
       <li>

-        <span class="date">Version 0.8.0 (2009-09).</span>
-      Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+        <span class="emph beta">Version 0.8.0 (2009-09).</span>
+      Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.

       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
       and exportation to <a href="http://www.w3.org/XML/">XML</a>.

-      <a href="http://lambdadelta.info/documentation.html#ldp6">Documentation</a>.
+      <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.

       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
       <ul>
           <li>
       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
       <ul>
           <li>


@@ -228,22 +214,22 @@
          for editing ".aut" files
          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
          for editing ".aut" files
          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>

-         (revised <span class="date">2008-07</span>).
+         (revised <span class="emph gamma">2008-07</span>).

       </li>
           <li>
       </li>
           <li>

-         <span class="date">2009-09.</span>
+            <span class="emph beta">2009-09.</span>

          Jutting's specification of Landau's "Grundlagen der Analysis"
          enters λδ Digital Library.
       </li>
           <li>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          enters λδ Digital Library.
       </li>
           <li>

-         <span class="date">2009-06.</span>
+            <span class="emph beta">2009-06.</span>

          Jutting's specification of Landau's "Grundlagen der Analysis"
          is successfully processed, enabling sort inclusion.
       </li>
         </ul>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          is successfully processed, enabling sort inclusion.
       </li>
         </ul>

-   </li>
+      </li>

     </ul>
     </ul>

-   <div class="spacer">
+    <div class="spacer">

       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">


@@ -269,6 +255,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
-</body>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+  </body>

 </html>
 </html>