From f16bf89d854b0c2658d6c622ef5f2bcb8a3cd45a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 10 Oct 2017 17:16:31 +0000 Subject: [PATCH] - web site update - update in ground_2 --- helm/www/lambdadelta/documentation.html | 4 +- helm/www/lambdadelta/download/lambdadelta.bib | 39 +++++---- helm/www/lambdadelta/download/lambdadelta.txt | 39 +++++---- helm/www/lambdadelta/ground_2.html | 86 ++++++++++++++++--- helm/www/lambdadelta/home.html | 9 +- helm/www/lambdadelta/specification.html | 4 +- .../web/home/documentation.ldw.xml | 2 +- helm/www/lambdadelta/web/home/home.ldw.xml | 6 ++ .../web/home/specification.ldw.xml | 2 +- 9 files changed, 136 insertions(+), 55 deletions(-) diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index dfd3d5ddf..4e087aa64 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -110,7 +110,7 @@ lambdadelta.bib, view lambdadelta.txt - (revised 2015-09). + (revised 2017-09).
[butterfly] λδ version 3 (proposed)
@@ -401,6 +401,6 @@

-
Last update: Sun, 16 Apr 2017 15:42:49 +0200
+
Last update: Tue, 10 Oct 2017 19:13:19 +0200
diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index 5e80745cf..70ddb4a96 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -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", @@ -10,13 +10,13 @@ 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", @@ -45,11 +45,11 @@ } @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", @@ -70,12 +70,12 @@ % \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", @@ -83,11 +83,14 @@ } @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", @@ -106,7 +109,7 @@ } @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", @@ -117,7 +120,7 @@ } @misc{lambdadeltaV1a, - author="F. {Guidi}", + author="Ferruccio {Guidi}", title="{lambdadelta\_1}", howpublished="Formal specification for the proof assistant Coq 7.3.1", year="2006", diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index 5e80745cf..70ddb4a96 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -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", @@ -10,13 +10,13 @@ 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", @@ -45,11 +45,11 @@ } @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", @@ -70,12 +70,12 @@ % \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", @@ -83,11 +83,14 @@ } @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", @@ -106,7 +109,7 @@ } @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", @@ -117,7 +120,7 @@ } @misc{lambdadeltaV1a, - author="F. {Guidi}", + author="Ferruccio {Guidi}", title="{lambdadelta\_1}", howpublished="Formal specification for the proof assistant Coq 7.3.1", year="2006", diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 2079a6198..68fa64dfc 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -132,29 +132,29 @@ sizes files - 95 + 102 characters - 135595 + 141898 nodes - 314345 + 327727 propositions theorems - 38 + 40 lemmas - 647 + 674 total - 685 + 714 concepts declared - 63 + 65 defined - 67 + 70 total - 130 + 135 @@ -254,6 +254,12 @@
+ +
+ + +
+
@@ -302,6 +308,12 @@
+ +
+ + +
+
@@ -312,10 +324,12 @@ rtmap rtmap_eq ( ? ≗ ? ) rtmap_pushs ( ↑*[?]? ) + rtmap_nexts ( ⫯*[?]? ) rtmap_tl ( ⫱? ) rtmap_tls ( ⫱*[?]? ) rtmap_isid ( 𝐈⦃?⦄ ) rtmap_id + rtmap_isdiv ( 𝛀⦃?⦄ ) rtmap_fcla ( 𝐂⦃?⦄ ≡ ? ) rtmap_isfin ( 𝐅⦃?⦄ ) rtmap_isuni ( 𝐔⦃?⦄ ) @@ -340,6 +354,7 @@ + nstream_isid nstream_id ( 𝐈𝐝 ) @@ -347,9 +362,10 @@ - nstream_sand + nstream_sor + nstream_istot ( ?@❴?❵ ) nstream_after ( ? ∘ ? ) nstream_coafter ( ? ~∘ ? ) @@ -404,6 +420,12 @@
+ +
+ + +
+
@@ -450,6 +472,12 @@
+ +
+ + +
+
@@ -500,6 +528,12 @@
+ +
+ + +
+
@@ -558,6 +592,12 @@
+ +
+ + +
+
@@ -616,6 +656,12 @@
+ +
+ + +
+
@@ -627,7 +673,8 @@
- star + relations + star lstar
@@ -674,6 +721,9 @@
+ +
+
@@ -728,6 +778,12 @@
+ +
+ + +
+
@@ -786,6 +842,12 @@
+ +
+ + +
+
@@ -819,6 +881,6 @@

-
Last update: Sun, 16 Apr 2017 15:42:49 +0200
+
Last update: Tue, 10 Oct 2017 19:10:34 +0200
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html index cdb00acd8..8473ef6ff 100644 --- a/helm/www/lambdadelta/home.html +++ b/helm/www/lambdadelta/home.html @@ -133,6 +133,13 @@
This is a list of publications citing λδ documentation.
+