web site update

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 5dd3febeb10889da37c2616d4086ac879d50062d..2756b021e17f39a01fae285bec1758ff2af58864 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -222,6 +222,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 11 Oct 2015 17:42:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 53f147170771b2be1a9e26746b1abc658734f59b..e6a410d4010bb6e741da50a07ef2a5396729e7ed 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Sep 2015 21:40:58 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index dbeb3de5d6e2319f8cf1ed2cb231ab9da533793d..46a2f63be113b052d2bf9d70472ab1a448384a7b 100644 (file)
--- 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: Sun, 11 Oct 2015 17:42:24 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:47 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index e7c85c8295e617dc7039f3513a8bccd28b62c49b..5dcb73a7735546f72d13877e925c994d0013b5a9 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -138,16 +138,16 @@
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      The main source of information is <span class="emph alpha">J2a</span>.
+      The main source of information is <span class="emph alpha">R2c</span>.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td class="snns top" id="ldJ2a">
-              <span class="emph alpha">J2a.</span>
+            <td class="snns top" id="ldR2c">
+              <span class="emph alpha">R2c.</span>
             </td>
-            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/basic2a.pdf">The Formal System λδ Revised, Stage A: Extending the Applicability Condition</a> (<span class="emph gamma">2014-11</span>). Preprint. CoRR identifier <a href="http://arxiv.org/abs/1411.0154">1411.0154</a> [v2] (revised <span class="emph gamma">2015-03</span>). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+            <td class="ssnn top">F. Guidi: <a href="http://amsacta.unibo.it/4411/">Extending the Applicability Condition in the Formal System λδ</a> (<span class="emph gamma">2015-03</span>). University of Bologna, technical report AMS Acta 4411. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
           <tr>
             <td class="nnns top" />
@@ -216,10 +216,10 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldV2">
-              <span class="emph alpha">V2.</span>
+            <td class="snns top" id="ldV2a">
+              <span class="emph alpha">V2a.</span>
             </td>
-            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_2.html">lambdadelta_2</a> (revised <span class="emph gamma">2014-10</span>). Formal specification for the proof assistant Matita 0.99.2 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_2.html">lambdadelta_2A1</a> (revised <span class="emph gamma">2014-10</span>). Formal specification for the proof assistant Matita 0.99.2 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
           <tr>
             <td class="nnss top" />
@@ -233,15 +233,15 @@
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      The main source of information is <span class="emph alpha">J1</span>.
+      The main source of information is <span class="emph alpha">J1a</span>.
       A summary is available in <span class="emph alpha">P1e</span>.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td class="snns top" id="ldJ1">
-              <span class="emph alpha">J1.</span>
+            <td class="snns top" id="ldJ1a">
+              <span class="emph alpha">J1a.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436">The Formal System λδ</a> (<span class="emph delta">2009-11</span>). In ACM ToCL 11(1), pp. 5:1-5:37 online app. pp. 1-11 (<a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
               <span class="emph delta">2008-07</span>). CoRR identifier <a href="http://arxiv.org/abs/cs/0611040">cs/0611040</a> [v10] (revised <span class="emph delta">2008-09</span>). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
@@ -349,8 +349,8 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldV1">
-              <span class="emph alpha">V1.</span>
+            <td class="snns top" id="ldV1a">
+              <span class="emph alpha">V1a.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_1.html">lambdadelta_1</a> (revised <span class="emph delta">2015-01</span>). Formal specification for the proof assistant Coq 7.3.1 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
@@ -389,6 +389,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 11 Oct 2015 17:42:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib
index 71e541b68306e6ba2c3cb1f3c582f531e5f85214..84ffa7d517520082f4fdb0c7fc1bb28de135c045 100644 (file)
--- a/helm/www/lambdadelta/download/lambdadelta.bib
+++ b/helm/www/lambdadelta/download/lambdadelta.bib
@@ -10,18 +10,29 @@
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ2a,
-   author="F. {Guidi}",
-   title="{The Formal System $\lambda\delta$ Revised, Stage A: Extending the Applicability Condition}",
-   howpublished="CoRR identifier 1411.0154",
-   year="2014",
-   month="November",
-   note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+%@misc{lambdadeltaJ2a,
+%   author="F. {Guidi}",
+%   title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}",
+%   howpublished="CoRR identifier 1411.0154",
+%   year="2014",
+%   month="November",
+%   note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+%}
+
+@techreport{lambdadeltaR2c,
+   author="F. {Guidi}", 
+   title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}",
+   type="Technical Report",
+   number="AMS Acta 4411",
+   institution="University of Bologna",
+   address="Bologna, Italy",
+   year="2015",
+   month="December"
 }
 
-@misc{lambdadeltaV2,
+@misc{lambdadeltaV2a,
    author="F. {Guidi}",
-   title="{lambdadelta\_2}",
+   title="{lambdadelta\_2A1}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
    year="2014",
    month="October",
@@ -53,7 +64,7 @@
 
 % \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@article{lambdadeltaJ1,
+@article{lambdadeltaJ1a,
    author="F. {Guidi}",
    title="{The Formal System $\lambda\delta$}",
    journal="Transactions on Computational Logic",
@@ -100,7 +111,7 @@
    month="January"
 }
 
-@misc{lambdadeltaV1,
+@misc{lambdadeltaV1a,
    author="F. {Guidi}",
    title="{lambdadelta\_1}",
    howpublished="Formal specification for the proof assistant Coq 7.3.1",

diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt
index 71e541b68306e6ba2c3cb1f3c582f531e5f85214..84ffa7d517520082f4fdb0c7fc1bb28de135c045 100644 (file)
--- a/helm/www/lambdadelta/download/lambdadelta.txt
+++ b/helm/www/lambdadelta/download/lambdadelta.txt
@@ -10,18 +10,29 @@
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadeltaJ2a,
-   author="F. {Guidi}",
-   title="{The Formal System $\lambda\delta$ Revised, Stage A: Extending the Applicability Condition}",
-   howpublished="CoRR identifier 1411.0154",
-   year="2014",
-   month="November",
-   note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+%@misc{lambdadeltaJ2a,
+%   author="F. {Guidi}",
+%   title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}",
+%   howpublished="CoRR identifier 1411.0154",
+%   year="2014",
+%   month="November",
+%   note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+%}
+
+@techreport{lambdadeltaR2c,
+   author="F. {Guidi}", 
+   title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}",
+   type="Technical Report",
+   number="AMS Acta 4411",
+   institution="University of Bologna",
+   address="Bologna, Italy",
+   year="2015",
+   month="December"
 }
 
-@misc{lambdadeltaV2,
+@misc{lambdadeltaV2a,
    author="F. {Guidi}",
-   title="{lambdadelta\_2}",
+   title="{lambdadelta\_2A1}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
    year="2014",
    month="October",
@@ -53,7 +64,7 @@
 
 % \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@article{lambdadeltaJ1,
+@article{lambdadeltaJ1a,
    author="F. {Guidi}",
    title="{The Formal System $\lambda\delta$}",
    journal="Transactions on Computational Logic",
@@ -100,7 +111,7 @@
    month="January"
 }
 
-@misc{lambdadeltaV1,
+@misc{lambdadeltaV1a,
    author="F. {Guidi}",
    title="{lambdadelta\_1}",
    howpublished="Formal specification for the proof assistant Coq 7.3.1",

diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz
deleted file mode 100644 (file)
index ff9bc83..0000000
Binary files a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz and /dev/null differ

diff --git a/helm/www/lambdadelta/download/lambdadelta_2A1.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2A1.tar.gz
new file mode 100644 (file)
index 0000000..ff9bc83
Binary files /dev/null and b/helm/www/lambdadelta/download/lambdadelta_2A1.tar.gz differ

diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index 84621a6e4636d0420d51c8eb777fe90d5ffe179d..5e96f04b453a1c7c9e6f6e5522b0004702d924bb 100644 (file)
--- 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: Sun, 11 Oct 2015 17:42:24 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:47 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 183932f93b271da7fed6367aa7804fb569dbeb49..9272c2a2adffd484290eb515c6768dcda2916c4c 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -359,6 +359,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 30 Oct 2015 12:45:15 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index c86890da2629845737637a56094d1735f48d5ebf..514477b52334ba32e5fecb6226fd686723824540 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -269,6 +269,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 11 Oct 2015 17:42:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 71db08c722335ad6d433e6543dddf704582c6c9d..0f1ce23d7f78e558d402c078b482a6fdb758dcaf 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -132,8 +132,15 @@
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="citations">Citations <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
-      This is a list of publications citing λδ (not including our own).
+      This is a list of publications citing λδ documentation.
    </div>
+    <ul xmlns:ld="http://lambdadelta.info/" id="C7">
+      <li>
+      C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
+      <span class="emph alpha">ELPI: fast, Embeddable, λProlog Interpreter</span>
+      (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468.
+   </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C6">
       <li>
       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
@@ -159,7 +166,7 @@
       <li>
       C.E. Brown:
       <span class="emph alpha">Faithful Reproductions of the Automath Landau Formalization</span>
-      (2011). Typescript note.
+      (2011). Technical report.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C2">
@@ -173,7 +180,7 @@
       <li>
       V. Rahili: 
       <span class="emph alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</span>
-      (July 2007). Typescript note.
+      (July 2007). Technical report.
    </li>
     </ul>
     <div class="spacer">
@@ -202,6 +209,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 11 Oct 2015 17:42:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 2e2f656c55804278d02cb4b906e1756df19a4366..01b480ffedb6eb27efdb1d26416b56ac901aaf74 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -105,6 +105,12 @@
     <!-- ===================================================================== -->
     <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 delta">August 2015.</span>
+      The specification of λδ version 2A1 is concluded.
+   </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph delta">March 2015.</span>
@@ -146,7 +152,7 @@
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph gamma">October 2014.</span>
-        <a href="http://lambdadelta.info/documentation.html#ldJ2a">λδ version 2A</a>
+        <a href="http://lambdadelta.info/documentation.html#ldJ2a">λδ version 2A1</a>
       is released.
    </li>
     </ul>
@@ -249,7 +255,7 @@
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph delta">July 2008.</span>
-        <a href="http://lambdadelta.info/documentation.html#ldJ1">First journal paper on λδ</a>
+        <a href="http://lambdadelta.info/documentation.html#ldJ1a">First journal paper on λδ</a>
       accepted for publication.
    </li>
     </ul>
@@ -354,6 +360,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 11 Oct 2015 17:42:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 2abf3281e503b4fbc8590c8bcbf7caa5a93115a3..4bc159e6ddce3e8c7342a420f291718711bd6977 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -133,7 +133,8 @@
             <td class="snnn top capitalize italic gray">started</td>
             <td class="snnn top capitalize italic gray">announced</td>
             <td class="snnn top capitalize italic gray">released</td>
-            <td class="ssnn top capitalize italic gray">concluded</td>
+            <td class="snnn top capitalize italic gray">concluded</td>
+            <td class="ssnn top capitalize italic gray">references</td>
           </tr>
           <tr>
             <td class="snns top orange">
@@ -143,11 +144,34 @@
             <td class="snnn top orange">
               <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
             </td>
-            <td class="snnn top orange">"A"</td>
+            <td class="snns top orange">"A2"</td>
+            <td class="snnn top orange">October 2015</td>
+            <td class="snnn top orange" />
+            <td class="snnn top orange" />
+            <td class="snnn top orange" />
+            <td class="ssnn top orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top orange">
+              <br />
+            </td>
+            <td class="nnnn top orange">
+              <br />
+            </td>
+            <td class="nnnn top orange">
+              <br />
+            </td>
+            <td class="snns top orange">"A1"</td>
             <td class="snnn top orange">April 2011</td>
             <td class="snnn top orange">June 2014</td>
             <td class="snnn top orange">October 2014</td>
-            <td class="ssnn top orange" />
+            <td class="snnn top orange">August 2015</td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/documentation#ldV2a">V2a</a>
+              <a href="http://lambdadelta.info/documentation#ldR2c">R2c</a>
+            </td>
           </tr>
           <tr>
             <td class="snns top orange">Abandoned</td>
@@ -159,7 +183,10 @@
             <td class="snnn top orange">March 2008</td>
             <td class="snnn top orange" />
             <td class="snnn top orange" />
-            <td class="ssnn top orange">February 2011</td>
+            <td class="snnn top orange">February 2011</td>
+            <td class="ssnn top orange">
+              <br />
+            </td>
           </tr>
           <tr>
             <td class="snss top red">
@@ -173,7 +200,11 @@
             <td class="snsn top red">May 2004</td>
             <td class="snsn top red">December 2005</td>
             <td class="snsn top red">November 2006</td>
-            <td class="sssn top red">May 2008</td>
+            <td class="snsn top red">May 2008</td>
+            <td class="sssn top red">
+              <a href="http://lambdadelta.info/documentation#ldV1a">V1a</a>
+              <a href="http://lambdadelta.info/documentation#ldJ1a">J1a</a>
+            </td>
           </tr>
         </tbody>
       </table>
@@ -208,9 +239,10 @@
     <ul xmlns:ld="http://lambdadelta.info/" id="source2">
       <li>
         <div class="text">
-          <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
+          <a href="http://lambdadelta.info/download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</a>
          (revised <span class="emph gamma">2014-10</span>).
          Source scripts.
+         <a href="http://lambdadelta.info/documentation.html#ldR2c">Documentation (R2c)</a>.
       </div>
         <div class="text">
          The scripts are grouped in directories, first by part, then by component.
@@ -242,6 +274,7 @@
           <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
          (revised <span class="emph delta">2015-09</span>).
          Source scripts.
+         <a href="http://lambdadelta.info/documentation.html#ldJ1a">Documentation (J1a)</a>.
          <ul>
             <li>
               <span class="emph delta">2015 January 15.</span>
@@ -328,6 +361,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 11 Oct 2015 17:42:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:21:42 +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 840d678eed92c649ad9357234f540c054ca95c4a..803bcbaf4e944d9210ee84823ce05d6e658ae13e 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -25,13 +25,13 @@
    
    <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
    <body>
-      The main source of information is <notice class="alpha" notice="J2a"/>.
+      The main source of information is <notice class="alpha" notice="R2c"/>.
    </body>
    <table name="documentation_2"/>
 
    <subsection name="v1"><version1-icon/>λδ version 1 (superseded)</subsection>
    <body>
-      The main source of information is <notice class="alpha" notice="J1"/>.
+      The main source of information is <notice class="alpha" notice="J1a"/>.
       A summary is available in <notice class="alpha" notice="P1e"/>.
    </body>
    <table name="documentation_1"/>

diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl
index c9ae8fa27e01ffeedb2ca54a06879aa37d917202..befe967a1d6e854999c9dadf5c9a9e623f9d031b 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_1.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_1.tbl
@@ -1,7 +1,7 @@
 name "documentation_1"
 
 table {
-   [ { name "ldJ1" "<span class=\"emph alpha\">J1.</span>" "" } {
+   [ { name "ldJ1a" "<span class=\"emph alpha\">J1a.</span>" "" } {
      "F. Guidi:" +
      @("http://doi.acm.org/10.1145/1614431.1614436"
      "The Formal System λδ") +
@@ -86,7 +86,7 @@ table {
      "<span class=\"emph alpha\">in Italian</span>)."
      * }
    ]
-   [ { name "ldV1" "<span class=\"emph alpha\">V1.</span>" "" } {
+   [ { name "ldV1a" "<span class=\"emph alpha\">V1a.</span>" "" } {
      "F. Guidi:" +
      @@("version_1.html" "lambdadelta_1") +
      "(revised <span class=\"emph delta\">2015-01</span>)." +

diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl
index 5d9e1e97d9f081046ca3704981d4f15a4d897a5a..c61d2b6a08f36847ad102afe149c77ead5901225 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_2.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_2.tbl
@@ -1,6 +1,7 @@
 name "documentation_2"
 
 table {
+(*
    [ { name "ldJ2a" "<span class=\"emph alpha\">J2a.</span>" "" } {
      "F. Guidi:" +
      @@("download/basic2a.pdf"
@@ -14,6 +15,16 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
+*)
+   [ { name "ldR2c" "<span class=\"emph alpha\">R2c.</span>" "" } {
+     "F. Guidi:" + 
+     @("http://amsacta.unibo.it/4411/"
+     "Extending the Applicability Condition in the Formal System λδ") +
+     "(<span class=\"emph gamma\">2015-03</span>)." +
+     "University of Bologna, technical report AMS Acta 4411." +
+     @@("documentation.html#bibtex" "BibTeX entry") ^ "."
+     * }
+   ]
    [ { name "ldR2b" "<span class=\"emph alpha\">R2b.</span>" "" } {
      "F. Guidi:" +
      @@("download/cie_2010.pdf"
@@ -57,9 +68,9 @@ table {
      "Presentation at University of Bologna (slides)."
      * }
    ]
-   [ { name "ldV2" "<span class=\"emph alpha\">V2.</span>" "" } {
+   [ { name "ldV2a" "<span class=\"emph alpha\">V2a.</span>" "" } {
      "F. Guidi:" +
-     @@("version_2.html" "lambdadelta_2") +
+     @@("version_2.html" "lambdadelta_2A1") +
      "(revised <span class=\"emph gamma\">2014-10</span>)." +
      "Formal specification for the proof assistant Matita 0.99.2 (scripts)." +
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."

diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml
index fce197c427308d40ac572bc1323b49f4a564fabd..d60da5f21e48f41878f5d5ff8830d7884c68dbb3 100644 (file)
--- a/helm/www/lambdadelta/web/home/index.ldw.xml
+++ b/helm/www/lambdadelta/web/home/index.ldw.xml
@@ -37,9 +37,15 @@
 
    <section9 name="citations">Citations</section9>
    <body>
-      This is a list of publications citing λδ (not including our own).
+      This is a list of publications citing λδ documentation.
    </body>
 
+   <topitem name="C7">
+      C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
+      <notice class="alpha" notice="ELPI: fast, Embeddable, λProlog Interpreter"/>
+      (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468.
+   </topitem>
+
    <topitem name="C6">
       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
       <notice class="alpha" notice="Formal metatheory of programming languages in the Matita interactive theorem prover"/>
@@ -61,7 +67,7 @@
    <topitem name="C3">
       C.E. Brown:
       <notice class="alpha" notice="Faithful Reproductions of the Automath Landau Formalization"/>
-      (2011). Typescript note.
+      (2011). Technical report.
    </topitem>
 
    <topitem name="C2">
@@ -73,7 +79,7 @@
    <topitem name="C1">
       V. Rahili: 
       <notice class="alpha" notice="First Year Report: Realisability methods of proof and semantics with application to expansion"/>
-      (July 2007). Typescript note.
+      (July 2007). Technical report.
    </topitem>
 
    <footer/>

diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml
index 46f208da9fe3e61d856f9ccaf1f55d5bb15c77e9..b14956cada6af005e42813ccc7c97799755002a2 100644 (file)
--- a/helm/www/lambdadelta/web/home/news.ldw.xml
+++ b/helm/www/lambdadelta/web/home/news.ldw.xml
@@ -11,6 +11,10 @@
 
    <section3 name="milestones">Milestones</section3>
 
+   <news class="delta" date="August 2015.">
+      The specification of λδ version 2A1 is concluded.
+   </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>.
@@ -38,7 +42,7 @@
    </news>
 
    <news class="gamma" date="October 2014.">
-      <rlink to="documentation.html#ldJ2a">λδ version 2A</rlink>
+      <rlink to="documentation.html#ldJ2a">λδ version 2A1</rlink>
       is released.
    </news>
 
@@ -109,7 +113,7 @@
    </news>
 
    <news class="delta" date="July 2008.">
-      <rlink to="documentation.html#ldJ1">First journal paper on λδ</rlink>
+      <rlink to="documentation.html#ldJ1a">First journal paper on λδ</rlink>
       accepted for publication.
    </news>
 

diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index 857516bcd66077257ddb2fd5fe583d968e714724..b88abf3a1c36290debcf6592226ffdc5ec4156b5 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -55,9 +55,10 @@
 
    <topitem name="source2">
       <body>
-         <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
+         <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
          (revised <notice class="gamma" notice="2014-10"/>).
          Source scripts.
+         <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
       </body>
       <body>
          The scripts are grouped in directories, first by part, then by component.
@@ -90,6 +91,7 @@
          <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
          (revised <notice class="delta" notice="2015-09"/>).
          Source scripts.
+         <rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
          <list><item>
             <notice class="delta" notice="2015 January 15."/>
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".

diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl
index b3cd3e0af4b3669f06436564a066c7cebadef0a7..5b7189241bde0e3ee99fbec6c1aa33f8fbbb100a 100644 (file)
--- a/helm/www/lambdadelta/web/home/versions.tbl
+++ b/helm/www/lambdadelta/web/home/versions.tbl
@@ -1,21 +1,31 @@
 name "versions"
 
 table {
-   class "gray"   
+   class "gray" 
       [ "version" "name" "developed with"
         "stage" "started" "announced" "released" "concluded"
+        "references"
       ]
-   class "orange" 
-      [ @@("specification#v2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
-        "\"A\"" "April 2011" "June 2014" "October 2014" ""
+   class "orange" {
+      [ { @@("specification#v2" "Version 2") * }
+        { "\"basic_2\"" * }
+        { @("http://matita.cs.unibo.it/" "Matita 0.99.2") * }
+        { [ "\"A2\"" "October 2015" "" "" ""
+            *
+          ]
+          [ "\"A1\"" "April 2011" "June 2014" "October 2014" "August 2015" 
+            @@("documentation#ldV2a" "V2a") + " " + @@("documentation#ldR2c" "R2c")
+          ]
+        }
       ]
-   class "orange"
       [ "Abandoned" "" @("http://coq.inria.fr/" "Coq 7.3.1")
-        "" "March 2008" "" "" "February 2011"
+        "" "March 2008" "" "" "February 2011" *
       ]
+   }
    class "red"
       [ @@("specification#v1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1")
         "" "May 2004" "December 2005" "November 2006" "May 2008"
+        @@("documentation#ldV1a" "V1a") + " " + @@("documentation#ldJ1a" "J1a")
       ]
 }