From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 30 Dec 2015 12:02:25 +0000 (+0000)
Subject: site update for helena 0.8.3
X-Git-Tag: make_still_working~667
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d966abb5707d0ce51be932b7bde99d4325d23a0c;p=helm.git

site update for helena 0.8.3
---

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index 46a2f63be..d64ee8ae3 100644
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -823,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:47 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 5dcb73a77..a60c9bbf9 100644
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -19,7 +19,7 @@
         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
       </a>
     </div>
-    <div class="head1">The Formal System λδ (\lambda\delta)</div>
+    <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -389,6 +389,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/download/helena_0.8.3.tar.gz b/helm/www/lambdadelta/download/helena_0.8.3.tar.gz
new file mode 100644
index 000000000..87ac1c2b3
Binary files /dev/null and b/helm/www/lambdadelta/download/helena_0.8.3.tar.gz differ
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index 5e96f04b4..205e37de7 100644
--- a/helm/www/lambdadelta/ground_1.html
+++ b/helm/www/lambdadelta/ground_1.html
@@ -275,6 +275,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:47 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 53a82992a..90f3bfd87 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -19,7 +19,7 @@
         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
       </a>
     </div>
-    <div class="head1">The Formal System λδ (\lambda\delta)</div>
+    <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -108,7 +108,7 @@
       <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">
       The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
-      and contains resources expressed in λδ.      
+      and contains resources expressed in the systems of the λδ family.      
    </div>
     <ul xmlns:ld="http://lambdadelta.info/" id="contents">
       <li>
@@ -136,10 +136,10 @@
     <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>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      Helena is a processor for λδ,
+      Helena is a processor for the systems of the λδ family,
       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.
+      meant for testing both their stable and unstable features.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       The processor source code is available in the directory
@@ -147,10 +147,32 @@
       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/" id="v3">
+      <li>
+        <span class="emph gamma">Version 0.8.3 (2015-12).</span>
+      Supports exportation to λProlog
+      (two formats for ELPI,
+      and two formats for <a href="http://teyjus.cs.umn.edu/">Teyjus</a>).
+      Employs optimized conditional compilation through
+      <a href="http://camlp5.gforge.inria.fr/">camlp5</a> code preprocessor (pa_macro)
+      to reduce a performance loss, which is expected to disappear
+      by employing a different code preprocessor.
+      Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
+      +3% with optimized compilation, +5% without optimized compilation.
+      [Svn revision: 13108] (<a href="http://lambdadelta.info/download/helena_0.8.3.tar.gz">archived source code</a>).
+      <ul>
+          <li>
+            <span class="emph gamma">2015-06.</span>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in a λProlog implementation of λδ version 3.
+      </li>
+        </ul>
+      </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="v2">
       <li>
         <span class="emph gamma">Version 0.8.2 (2015-02).</span>
-      Uses λδ "Version 3" with layer variables as core language.
+      Uses λδ version 3 with layer variables as core language.
       Supports exportation to Gallina
       (the specification language of <a href="http://coq.inria.fr/">Coq</a>),
       and to Grafite
@@ -185,7 +207,7 @@
           <li>
             <span class="emph gamma">2014-12.</span>
          The corrected specification of Landau's "Grundlagen der Analysis"
-         is successfully validated in λδ "Version 3".
+         is successfully validated in λδ version 3.
       </li>
         </ul>
       </li>
@@ -193,7 +215,7 @@
     <ul xmlns:ld="http://lambdadelta.info/" id="v1">
       <li>
         <span class="emph beta">Version 0.8.1 (2010-11).</span>
-      Uses a subset of λδ "Version 4" as intermediate language.
+      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"
       increases of 22% with respect to version 0.8.0.
@@ -217,7 +239,7 @@
     <ul xmlns:ld="http://lambdadelta.info/" id="v0">
       <li>
         <span class="emph beta">Version 0.8.0 (2009-09).</span>
-      Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
+      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>.
       <a href="http://lambdadelta.info/documentation.html#ldR2a">Documentation (R2a)</a>.
@@ -269,6 +291,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 18:24:26 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 0f1ce23d7..8a582d04c 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -19,7 +19,7 @@
         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
       </a>
     </div>
-    <div class="head1">The Formal System λδ (\lambda\delta)</div>
+    <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -105,19 +105,18 @@
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Foreword <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+      The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
       the foundational frameworks for Mathematics that require an underlying specification language
       (for example the <a href="http://www.math.unipd.it/~maietti/">Minimalist Foundation</a>
        and its predecessors).
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      λδ is developed in the context of the
+      The λδ family is developed within the
       <a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
-      as a machine-checked digital specification
-      that is not the formal counterpart of previous informal material.
+      as a set of machine-checked digital specifications.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      This is the System logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
+      This is the family logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
       (revised <span class="emph alpha">2012-09</span>).
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -181,6 +180,74 @@
       V. Rahili: 
       <span class="emph alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</span>
       (July 2007). Technical report.
+   </li>
+    </ul>
+    <!-- ===================================================================== -->
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The systens of the λδ family <span xmlns="http://lambdadelta.info/" class="emph">are not</span> related intentionally to any other system
+      having (variations of) the symbols λ and δ in its name or syntax.
+      Examples include (but are not limited to):
+   </div>
+    <ul xmlns:ld="http://lambdadelta.info/" id="D1">
+      <li>
+        <span xmlns="http://lambdadelta.info/" class="emph">λ-δ</span> of
+      A. Church:
+      <span xmlns="http://lambdadelta.info/" class="emph">The calculi of lambda-conversion</span>
+      (1941).
+      Annals of Mathematics Studies 6.
+      Princeton University Press.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/" id="D2">
+      <li>
+        <span xmlns="http://lambdadelta.info/" class="emph">∆Λ</span> of
+      N.G. de Bruijn:
+      <span xmlns="http://lambdadelta.info/" class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+      (1987).
+      In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+      Marcel Dekker.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/" id="D3">
+      <li>
+        <span xmlns="http://lambdadelta.info/" class="emph">λ<sub>∆</sub>
+        </span> of
+      N.J. Rehof, M.H. Sørensen:
+      <span xmlns="http://lambdadelta.info/" class="emph">The λ<sub>∆</sub>-calculus</span>
+      (1994).
+      In Lecture Notes in Computer Science, 789, pp. 516–542.
+      Springer.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/" id="D4">
+      <li>
+        <span xmlns="http://lambdadelta.info/" class="emph alpha">λ∆</span> of
+      S. Ronchi Della Rocca, L. Paolini:
+      <span xmlns="http://lambdadelta.info/" class="emph">The Parametric Lambda Calculus</span>
+      (2004).
+      Texts in Theoretical Computer Science, An EATCS Series.
+      Springer.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/" id="D5">
+      <li>
+        <span xmlns="http://lambdadelta.info/" class="emph">λD</span> of
+      R. Nederpelt, H. Geuvers:
+      <span xmlns="http://lambdadelta.info/" class="emph">Type Theory and Formal Proof</span>
+      (2014).
+      Cambridge University Press.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/" id="D6">
+      <li>
+        <span xmlns="http://lambdadelta.info/" class="emph">Cλξ</span> of
+      N.G. de Bruijn:
+      <span xmlns="http://lambdadelta.info/" class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+      (1978).
+      TH-report 78-WSK-03.
+      Eindhoven University of Technology, Eindhoven.
    </li>
     </ul>
     <div class="spacer">
@@ -209,6 +276,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index b77c6b4cf..02ed66ceb 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -19,7 +19,7 @@
         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
       </a>
     </div>
-    <div class="head1">The Formal System λδ (\lambda\delta)</div>
+    <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -105,10 +105,23 @@
     <!-- ===================================================================== -->
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
     </div>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph gamma">December 2015.</span>
+        <a href="http://lambdadelta.info/implementation.html#v3">"Helena 0.8.3"</a> is released.
+   </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph delta">August 2015.</span>
       The specification of λδ version 2A1 is concluded.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph gamma">June 2015.</span>
+      The corrected specification of Landau's "Grundlagen der Analysis"
+      is validated in a λProlog implementation of λδ version 3.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
@@ -323,7 +336,7 @@
         <span class="emph alpha">June 2014.</span>
       The <a href="http://www.google.com/">Google</a>
       search for "formal system lambda delta" gives
-      5 resources about λδ in the first 6 results.
+      5 resources about the λδ family in the first 6 results.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
@@ -331,7 +344,7 @@
         <span class="emph alpha">June 2014.</span>
       The <a href="http://www.yahoo.com/">Yahoo</a>
       search for "formal system lambda delta" gives
-      4 resources about λδ in the first 5 results.
+      4 resources about the λδ family in the first 5 results.
    </li>
     </ul>
     <div class="spacer">
@@ -360,6 +373,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 18:24:26 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:03 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 4bc159e6d..ee93a0f9a 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -19,7 +19,7 @@
         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
       </a>
     </div>
-    <div class="head1">The Formal System λδ (\lambda\delta)</div>
+    <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -105,9 +105,8 @@
     <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/b15.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      λδ is developed as a machine-checked digital specification.
-      It comes in several versions listed in the next table,
-      which includes the major milestones.
+      The systems of the λδ family are developed as machine-checked digital specifications,
+      and are listed in the next table, which includes the major milestones.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       The life cycle of a specification consists of four periods.
@@ -361,6 +360,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:21:42 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml
index 803bcbaf4..db2189cc6 100644
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -3,7 +3,7 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index ef29ccc0f..bd3f4e23b 100644
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -3,7 +3,7 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
@@ -12,7 +12,7 @@
    <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
    <body>
       The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
-      and contains resources expressed in λδ.      
+      and contains resources expressed in the systems of the λδ family.      
    </body>
    <topitem name="contents">
       <notice class="alpha" notice="Contents:"/>
@@ -33,11 +33,12 @@
    </topitem>
 
    <subsection name="helena"><helena-icon/>Helena</subsection>
+
    <body>
-      Helena is a processor for λδ,
+      Helena is a processor for the systems of the λδ family,
       implemented in <link to="http://caml.inria.fr/">Caml</link>
       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
-      meant for testing the stable features of the calculus as well as the unstable ones.
+      meant for testing both their stable and unstable features.
    </body>
    <body>
       The processor source code is available in the directory
@@ -45,9 +46,29 @@
       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
       The Svn revisions containing the stable versions of Helena are indicated next.
    </body>
+
+   <topitem name="v3">
+      <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
+      Supports exportation to λProlog
+      (two formats for ELPI,
+      and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
+      Employs optimized conditional compilation through
+      <link to="http://camlp5.gforge.inria.fr/">camlp5</link> code preprocessor (pa_macro)
+      to reduce a performance loss, which is expected to disappear
+      by employing a different code preprocessor.
+      Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
+      +3% with optimized compilation, +5% without optimized compilation.
+      [Svn revision: 13108] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
+      <list><item>
+         <notice class="gamma" notice="2015-06."/>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in a λProlog implementation of λδ version 3.
+      </item></list>
+   </topitem>
+
    <topitem name="v2">
       <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
-      Uses λδ "Version 3" with layer variables as core language.
+      Uses λδ version 3 with layer variables as core language.
       Supports exportation to Gallina
       (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
       and to Grafite
@@ -77,12 +98,13 @@
       </item><item>
          <notice class="gamma" notice="2014-12."/>
          The corrected specification of Landau's "Grundlagen der Analysis"
-         is successfully validated in λδ "Version 3".
+         is successfully validated in λδ version 3.
       </item></list>
    </topitem>
+
    <topitem name="v1">
       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
-      Uses a subset of λδ "Version 4" as intermediate language.
+      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"
       increases of 22% with respect to version 0.8.0.
@@ -99,9 +121,10 @@
             index of computer math systems</link>.
       </item></list>
    </topitem>
+
    <topitem name="v0">
       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
-      Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
+      Supports λδ version 2 with naive implementation of impredicative sort inclusion.
       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
       <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
@@ -122,5 +145,6 @@
          is successfully processed, enabling sort inclusion.
       </item></list>
    </topitem>
+
    <footer/>
 </page>
diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml
index d60da5f21..9ebac8e80 100644
--- a/helm/www/lambdadelta/web/home/index.ldw.xml
+++ b/helm/www/lambdadelta/web/home/index.ldw.xml
@@ -3,25 +3,24 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
    <section9 name="foreword">Foreword</section9>
    <body>
-      The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+      The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
       the foundational frameworks for Mathematics that require an underlying specification language
       (for example the <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
        and its predecessors).
    </body>
    <body>
-      λδ is developed in the context of the
+      The λδ family is developed within the
       <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
-      as a machine-checked digital specification
-      that is not the formal counterpart of previous informal material.
+      as a set of machine-checked digital specifications.
    </body>
    <body>
-      This is the System logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
+      This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
       (revised <notice class="alpha" notice="2012-09"/>).
    </body>
    <body>
@@ -82,5 +81,67 @@
       (July 2007). Technical report.
    </topitem>
 
+<!-- ===================================================================== -->
+
+   <section9 name="disclaimer">Disclaimer</section9>
+   <body>
+      The systens of the λδ family <span class="emph">are not</span> related intentionally to any other system
+      having (variations of) the symbols λ and δ in its name or syntax.
+      Examples include (but are not limited to):
+   </body>
+
+   <topitem name="D1">
+      <span class="emph">λ-δ</span> of
+      A. Church:
+      <span class="emph">The calculi of lambda-conversion</span>
+      (1941).
+      Annals of Mathematics Studies 6.
+      Princeton University Press.
+   </topitem>
+
+   <topitem name="D2">
+      <span class="emph">∆Λ</span> of
+      N.G. de Bruijn:
+      <span class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+      (1987).
+      In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
+      Marcel Dekker.
+   </topitem>
+
+   <topitem name="D3">
+      <span class="emph">λ<sub>∆</sub></span> of
+      N.J. Rehof, M.H. Sørensen:
+      <span class="emph">The λ<sub>∆</sub>-calculus</span>
+      (1994).
+      In Lecture Notes in Computer Science, 789, pp. 516–542.
+      Springer.
+   </topitem>
+
+   <topitem name="D4">
+      <span class="emph alpha">λ∆</span> of
+      S. Ronchi Della Rocca, L. Paolini:
+      <span class="emph">The Parametric Lambda Calculus</span>
+      (2004).
+      Texts in Theoretical Computer Science, An EATCS Series.
+      Springer.
+   </topitem>
+
+   <topitem name="D5">
+      <span class="emph">λD</span> of
+      R. Nederpelt, H. Geuvers:
+      <span class="emph">Type Theory and Formal Proof</span>
+      (2014).
+      Cambridge University Press.
+   </topitem>
+
+   <topitem name="D6">
+      <span class="emph">Cλξ</span> of
+      N.G. de Bruijn:
+      <span class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+      (1978).
+      TH-report 78-WSK-03.
+      Eindhoven University of Technology, Eindhoven.
+   </topitem>
+
    <footer/>
 </page>
diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml
index 1208fb9c0..966e0fa4c 100644
--- a/helm/www/lambdadelta/web/home/news.ldw.xml
+++ b/helm/www/lambdadelta/web/home/news.ldw.xml
@@ -3,7 +3,7 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
@@ -11,10 +11,19 @@
 
    <section3 name="milestones">Milestones</section3>
 
+   <news class="gamma" date="December 2015.">
+      <rlink to="implementation.html#v3">"Helena 0.8.3"</rlink> is released.
+   </news>
+
    <news class="delta" date="August 2015.">
       The specification of λδ version 2A1 is concluded.
    </news>
 
+   <news class="gamma" date="June 2015.">
+      The corrected specification of Landau's "Grundlagen der Analysis"
+      is validated in a λProlog implementation of λδ version 3.
+   </news>
+
    <news class="delta" date="March 2015.">
       The specification of λδ version 1 is validated by
       <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>.
@@ -164,13 +173,13 @@
    <news class="alpha" date="June 2014.">
       The <link to="http://www.google.com/">Google</link>
       search for "formal system lambda delta" gives
-      5 resources about λδ in the first 6 results.
+      5 resources about the λδ family in the first 6 results.
    </news>
 
    <news class="alpha" date="June 2014.">
       The <link to="http://www.yahoo.com/">Yahoo</link>
       search for "formal system lambda delta" gives
-      4 resources about λδ in the first 5 results.
+      4 resources about the λδ family in the first 5 results.
    </news>
 
    <footer/>
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index b88abf3a1..e8c3d5b13 100644
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -3,15 +3,14 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
    <section15 name="specifications">Computer-checked formal specifications</section15>
    <body>
-      λδ is developed as a machine-checked digital specification.
-      It comes in several versions listed in the next table,
-      which includes the major milestones.
+      The systems of the λδ family are developed as machine-checked digital specifications,
+      and are listed in the next table, which includes the major milestones.
    </body>
    <body>
       The life cycle of a specification consists of four periods.