]> matita.cs.unibo.it Git - helm.git/commitdiff
- web site update
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 10 Oct 2017 17:16:31 +0000 (17:16 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 10 Oct 2017 17:16:31 +0000 (17:16 +0000)
- update in ground_2

helm/www/lambdadelta/documentation.html
helm/www/lambdadelta/download/lambdadelta.bib
helm/www/lambdadelta/download/lambdadelta.txt
helm/www/lambdadelta/ground_2.html
helm/www/lambdadelta/home.html
helm/www/lambdadelta/specification.html
helm/www/lambdadelta/web/home/documentation.ldw.xml
helm/www/lambdadelta/web/home/home.ldw.xml
helm/www/lambdadelta/web/home/specification.ldw.xml

index dfd3d5ddfd729320f65fc856b2cb9791ad1ae44d..4e087aa640df1022e780b4f05c968af3abc005dd 100644 (file)
       <a href="http://lambdadelta.info/download/lambdadelta.bib">lambdadelta.bib</a>,
       <span class="emph alpha">view</span>
       <a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
-      (revised <span class="emph gamma">2015-09</span>).
+      (revised <span class="emph gamma">2017-09</span>).
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v3">
       <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b8.png" /> λδ version 3 (proposed)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 16 Apr 2017 15:42:49 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 10 Oct 2017 19:13:19 +0200</div>
   </body>
 </html>
index 5e80745cf383fe1f7afde3807e02f3de6646cac3..70ddb4a9662f5ec18e9bf85f73716a4ed1c97977 100644 (file)
@@ -1,7 +1,7 @@
 % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 @article{lambdadeltaJ3a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{Verified Representations of Landau's ``Grundlagen'' in the $\lambda\delta$ Family and in the Calculus of Constructions}",
    Publisher="University of Bologna",
    address="Bologna, Italy",
    number="1",
    year="2015",
    month="December",
-   pages="93-116"
+   pages="93--116"
 }
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 @comment{lambdadeltaJ2a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}",
    howpublished="CoRR identifier 1411.0154",
    year="2014",
@@ -25,7 +25,7 @@
 }
 
 @techreport{lambdadeltaR2c,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}",
    type="Technical Report",
    number="AMS Acta 4411",
@@ -36,7 +36,7 @@
 }
 
 @misc{lambdadeltaV2a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{lambdadelta\_2A1}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
    year="2014",
 }
 
 @incollection{lambdadeltaR2b,
-   author="F. {Guidi}", 
-   title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
-   editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
+   author="Ferruccio {Guidi}", 
+   title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}"
+   editor="Fernando {Ferreira} and H\'elia {Guerra} and Elvira {Mayordomo} and Jo\~ao {Rasga}",
    booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)",
-   pages="204-213",
+   pages="204--213",
    publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores",
    address="Ponta Delgada, Portugal",
    year="2010",
@@ -57,7 +57,7 @@
 }
 
 @techreport{lambdadeltaR2a,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", 
    type="Technical Report",
    number="UBLCS 2009-16",
 % \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 @article{lambdadeltaJ1a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{The Formal System $\lambda\delta$}",
    journal="Transactions on Computational Logic",
    volume="11",
    number="1",
-   pages="5:1-5:37, online appendix 1-11",
+   pages="5:1--5:37, online appendix 1--11",
    publisher="ACM",
    address="New York, NY, USA",
    year="2009",
 }
 
 @incollection{lambdadeltaR1c,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}",
+
+
    title="{Lambda Types on the Lambda Calculus with Abbreviations}",
-   editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
+   editor="Stuart Barry {Cooper} and Thomas F. {Kent} and Benedikt {L\"owe} and Andrea {Sorbi}", @comment="{\"}",
    booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487",
-   pages="387-387",
+   pages="387--387",
    publisher="Universit\`a di Siena",
    address="Siena, Italy",
    year="2007",
@@ -95,7 +98,7 @@
 }
 
 @techreport{lambdadeltaR1b,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", 
    type="Technical Report",
    number="UBLCS 2006-25",
 }
 
 @techreport{lambdadeltaR1a,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", 
    type="Technical Report",
    number="UBLCS 2006-01",
 }
 
 @misc{lambdadeltaV1a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{lambdadelta\_1}",
    howpublished="Formal specification for the proof assistant Coq 7.3.1",
    year="2006",
index 5e80745cf383fe1f7afde3807e02f3de6646cac3..70ddb4a9662f5ec18e9bf85f73716a4ed1c97977 100644 (file)
@@ -1,7 +1,7 @@
 % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 @article{lambdadeltaJ3a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{Verified Representations of Landau's ``Grundlagen'' in the $\lambda\delta$ Family and in the Calculus of Constructions}",
    Publisher="University of Bologna",
    address="Bologna, Italy",
    number="1",
    year="2015",
    month="December",
-   pages="93-116"
+   pages="93--116"
 }
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 @comment{lambdadeltaJ2a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}",
    howpublished="CoRR identifier 1411.0154",
    year="2014",
@@ -25,7 +25,7 @@
 }
 
 @techreport{lambdadeltaR2c,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}",
    type="Technical Report",
    number="AMS Acta 4411",
@@ -36,7 +36,7 @@
 }
 
 @misc{lambdadeltaV2a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{lambdadelta\_2A1}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
    year="2014",
 }
 
 @incollection{lambdadeltaR2b,
-   author="F. {Guidi}", 
-   title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
-   editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
+   author="Ferruccio {Guidi}", 
+   title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}"
+   editor="Fernando {Ferreira} and H\'elia {Guerra} and Elvira {Mayordomo} and Jo\~ao {Rasga}",
    booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)",
-   pages="204-213",
+   pages="204--213",
    publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores",
    address="Ponta Delgada, Portugal",
    year="2010",
@@ -57,7 +57,7 @@
 }
 
 @techreport{lambdadeltaR2a,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", 
    type="Technical Report",
    number="UBLCS 2009-16",
 % \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 @article{lambdadeltaJ1a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{The Formal System $\lambda\delta$}",
    journal="Transactions on Computational Logic",
    volume="11",
    number="1",
-   pages="5:1-5:37, online appendix 1-11",
+   pages="5:1--5:37, online appendix 1--11",
    publisher="ACM",
    address="New York, NY, USA",
    year="2009",
 }
 
 @incollection{lambdadeltaR1c,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}",
+
+
    title="{Lambda Types on the Lambda Calculus with Abbreviations}",
-   editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
+   editor="Stuart Barry {Cooper} and Thomas F. {Kent} and Benedikt {L\"owe} and Andrea {Sorbi}", @comment="{\"}",
    booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487",
-   pages="387-387",
+   pages="387--387",
    publisher="Universit\`a di Siena",
    address="Siena, Italy",
    year="2007",
@@ -95,7 +98,7 @@
 }
 
 @techreport{lambdadeltaR1b,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", 
    type="Technical Report",
    number="UBLCS 2006-25",
 }
 
 @techreport{lambdadeltaR1a,
-   author="F. {Guidi}", 
+   author="Ferruccio {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", 
    type="Technical Report",
    number="UBLCS 2006-01",
 }
 
 @misc{lambdadeltaV1a,
-   author="F. {Guidi}",
+   author="Ferruccio {Guidi}",
    title="{lambdadelta\_1}",
    howpublished="Formal specification for the proof assistant Coq 7.3.1",
    year="2006",
index 2079a61983f5e6505330971996b38e53b6701eb2..68fa64dfc9243140890b050be20ce23bf7a7cb77 100644 (file)
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">95</td>
+            <td class="snnn right italic cyan">102</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">135595</td>
+            <td class="snnn right italic cyan">141898</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">314345</td>
+            <td class="ssnn right italic cyan">327727</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">38</td>
+            <td class="snnn right italic green">40</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">647</td>
+            <td class="snnn right italic green">674</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">685</td>
+            <td class="ssnn right italic green">714</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">63</td>
+            <td class="snsn right italic yellow">65</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">67</td>
+            <td class="snsn right italic yellow">70</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">130</td>
+            <td class="sssn right italic yellow">135</td>
           </tr>
         </tbody>
       </table>
             <td class="snnn top gray">
               <br />
             </td>
+            <td class="snnn top gray">
+              <br />
+            </td>
+            <td class="snnn top gray">
+              <br />
+            </td>
             <td class="ssnn top gray">
               <br />
             </td>
             <td class="snnn top water">
               <br />
             </td>
+            <td class="snnn top water">
+              <br />
+            </td>
+            <td class="snnn top water">
+              <br />
+            </td>
             <td class="ssnn top water">
               <br />
             </td>
             <td class="snns top green">rtmap</td>
             <td class="snnn top green">rtmap_eq ( ? ≗ ? )</td>
             <td class="snnn top green">rtmap_pushs ( ↑*[?]? )</td>
+            <td class="snnn top green">rtmap_nexts ( ⫯*[?]? )</td>
             <td class="snnn top green">rtmap_tl ( ⫱? )</td>
             <td class="snnn top green">rtmap_tls ( ⫱*[?]? )</td>
             <td class="snnn top green">rtmap_isid ( 𝐈⦃?⦄ )</td>
             <td class="snnn top green">rtmap_id</td>
+            <td class="snnn top green">rtmap_isdiv ( 𝛀⦃?⦄ )</td>
             <td class="snnn top green">rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )</td>
             <td class="snnn top green">rtmap_isfin ( 𝐅⦃?⦄ )</td>
             <td class="snnn top green">rtmap_isuni ( 𝐔⦃?⦄ )</td>
             <td class="snnn top green" />
             <td class="snnn top green" />
             <td class="snnn top green" />
+            <td class="snnn top green" />
             <td class="snnn top green">nstream_isid</td>
             <td class="snnn top green">nstream_id ( 𝐈𝐝 )</td>
             <td class="snnn top green" />
             <td class="snnn top green" />
             <td class="snnn top green" />
             <td class="snnn top green" />
-            <td class="snnn top green">nstream_sand</td>
             <td class="snnn top green" />
             <td class="snnn top green" />
+            <td class="snnn top green">nstream_sor</td>
+            <td class="snnn top green" />
             <td class="snnn top green">nstream_istot ( ?@❴?❵ )</td>
             <td class="snnn top green">nstream_after ( ? ∘ ? )</td>
             <td class="ssnn top green">nstream_coafter ( ? ~∘ ? )</td>
             <td class="snnn top green">
               <br />
             </td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="snnn top green">
+              <br />
+            </td>
             <td class="ssnn top green">
               <br />
             </td>
             <td class="snnn top grass">
               <br />
             </td>
+            <td class="snnn top grass">
+              <br />
+            </td>
+            <td class="snnn top grass">
+              <br />
+            </td>
             <td class="ssnn top grass">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="nnns top italic yellow">
               <br />
             </td>
-            <td class="snns top yellow">star</td>
+            <td class="snns top yellow">relations</td>
+            <td class="snnn top yellow">star</td>
             <td class="snnn top yellow">lstar</td>
             <td class="snnn top yellow">
               <br />
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top orange">
               <br />
             </td>
+            <td class="snnn top orange">
+              <br />
+            </td>
+            <td class="snnn top orange">
+              <br />
+            </td>
             <td class="ssnn top orange">
               <br />
             </td>
             <td class="snsn top red">
               <br />
             </td>
+            <td class="snsn top red">
+              <br />
+            </td>
+            <td class="snsn top red">
+              <br />
+            </td>
             <td class="sssn top red">
               <br />
             </td>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 16 Apr 2017 15:42:49 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 10 Oct 2017 19:10:34 +0200</div>
   </body>
 </html>
index cdb00acd8a4721a7a82b6bf68e082674097b7651..8473ef6ff0dc8b608637bb730e33cc5eb350706d 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       This is a list of publications citing λδ documentation.
    </div>
+    <ul xmlns:ld="http://lambdadelta.info/" id="C9">
+      <li>
+      Matthias Weber:
+      <span class="emph alpha">An extended type system with lambda-typed lambda-expressions (extended version)</span>
+      (2017). Technical report. Faculty of Computer Science, Technical University of Berlin.
+   </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C8">
       <li>
       M.E. Maietti, S. Maschio:
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 16 Apr 2017 15:42:49 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 10 Oct 2017 19:10:32 +0200</div>
   </body>
 </html>
index 07d6ecf3beb8c321d803750d1a50790c8d2a90f7..37a13819a7186f5d6b68b526dec6fdf4628b59e6 100644 (file)
         <div class="text">
           <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.
+         Source scripts [Svn revision: 12964].
          <a href="http://lambdadelta.info/documentation.html#ldR2c">Documentation (R2c)</a>.
       </div>
         <div class="text">
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 16 Apr 2017 15:42:49 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 10 Oct 2017 19:10:33 +0200</div>
   </body>
 </html>
index 6ce59cb7957409a7feed7f8853cea333a4fe2169..76725fda4f6ef7445152e8ec9a58a078351bd6da 100644 (file)
@@ -15,7 +15,7 @@
       <rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
       <notice class="alpha" notice="view"/>
       <rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
-      (revised <notice class="gamma" notice="2015-09"/>).
+      (revised <notice class="gamma" notice="2017-09"/>).
    </body>
 
    <subsection name="v3"><img logo="ld3"/>λδ version 3 (proposed)</subsection>
index f62d71288b8f9b99ae6e91758998c7e1a8ae69c3..253ecd6b7e48a5ec549930f2b146ac63ac1143d6 100644 (file)
       This is a list of publications citing λδ documentation.
    </body>
 
+   <topitem name="C9">
+      Matthias Weber:
+      <notice class="alpha">An extended type system with lambda-typed lambda-expressions (extended version)</notice>
+      (2017). Technical report. Faculty of Computer Science, Technical University of Berlin.
+   </topitem>
+
    <topitem name="C8">
       M.E. Maietti, S. Maschio:
       <notice class="alpha">An extensional Kleene realizability semantics for the Minimalist Foundation</notice>
index e3f4baf3bf5a29039b5ba52aee0bbbd51025f8f6..10a24009f6f08c8d3f03d5964e486e8c5b39d21c 100644 (file)
@@ -65,7 +65,7 @@
       <body>
          <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
          (revised <notice class="gamma" text="2014-10"/>).
-         Source scripts.
+         Source scripts [Svn revision: 12964].
          <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
       </body>
       <body>