site update for helena 0.8.3

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

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 0f1ce23d7f78e558d402c078b482a6fdb758dcaf..8a582d04c4bc8ae17bdaff2e8c444b7a9c8c9682 100644 (file)
--- 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>