From 7f349a4f0175068138a341081d0dd14fd9fe4c4a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 20 Jul 2014 09:40:28 +0000 Subject: [PATCH] - update in ground_2 and basic_2 - the third page of the web site is generated --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/Makefile | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 2 +- helm/www/lambdadelta/documentation.html | 507 +++++++++--------- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/index.html | 40 +- helm/www/lambdadelta/news.html | 40 +- helm/www/lambdadelta/version_1.html | 40 +- helm/www/lambdadelta/version_2.html | 40 +- .../web/home/documentation.ldw.xml | 32 ++ .../lambdadelta/web/home/documentation_1.tbl | 91 ++++ .../lambdadelta/web/home/documentation_2.tbl | 57 ++ helm/www/lambdadelta/web/home/sitemap.tbl | 15 +- 14 files changed, 512 insertions(+), 360 deletions(-) create mode 100644 helm/www/lambdadelta/web/home/documentation.ldw.xml create mode 100644 helm/www/lambdadelta/web/home/documentation_1.tbl create mode 100644 helm/www/lambdadelta/web/home/documentation_2.tbl diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 49c40f274..9b46aa52c 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:33 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index c88300d95..4c610a09a 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -88,7 +88,7 @@ endif all: www -www: $(HTMLS) +www: $(HTMLS) $(TBLS) $(XHTBL) lint-xml: $(XMLS:%=$(XMLDIR)/%) @echo XMLLINT --valid diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index afa107af9..ece3b07ca 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:32 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 54deb5321..9595ea5b3 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1300,6 +1300,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:32 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 56ff9c6fb..e41618049 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -1,303 +1,332 @@ - - - - - λδ home page - - - - - -

-[Crux Logo] -

The Formal System λδ (\lambda\delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
- - -
    -
  • Papers
  • -
- -
-

Documentation [Butterfly]

-

[Basic
-                  lambdadelta Logo] Basic λδ version -2 (in progress):

-The main source of -information is Resource P8.
-
- + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ (\lambda\delta)
+
+ [Spacer] +
+
+
+
+
+
- - + + + - + + + + - + + + + + + + + +
R5.
+
+ home F. -Guidi: An Efficient Validation Procedure for the -Formal System λδ (2010-07). - -In - - CiE 2010 Local Proceedings. - -University -of -Azores, CMATI Booklet, pp. 204-213. BibTeX entry.
-
+
+ news + + documentation + + implementation + +
R4.
+
+ Foreword + + Milestones + + Version 2 + + Version 2 + + Background + Core + Applications F. -Guidi: Landau's "Grundlagen der Analysis" from -Automath to lambda-delta (2009-09). +
+ Notice + + Visibility + + Version 1 + + Version 1 + +
+
+ -University -of -Bologna, technical report UBLCS-2009-16. BibTeX entry.
-

-
+
Documentation [spacer] +
+
+ BibTeX database of λδ documentation: + lambdadelta.bib, + lambdadelta.txt + (revised 2012-10). +
+ +
+ [basic lambdadelta] λδ version 2 (in progress)
+
+ The main source of information is P8. +
+
+ + + + + - - + + + - - + + + + + + + + + + + + + + + + + + + + - + + + + -
+ R5. F. Guidi: An Efficient Validation Procedure for the Formal System λδ (2010-07). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry.
P8.
+
+ +
F.Guidi: - The Formal System λδ and the "Three -Problems" (2014-06). -Presentation at University of Bologna (slides).
-
+
+ R4. F. Guidi: Landau's "Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of Bologna, technical report UBLCS-2009-16. BibTeX entry.
P7.
+
+ +
F. -Guidi: An Efficient Validation Procedure for the -Formal System λδ (2010-07). - -Presentation -at -CiE 2010 (slides).
-
+
+ P8. + F. Guidi: The Formal System λδ and the "Three Problems" (2014-06). Presentation at University of Bologna (slides).
+ +
+
+ P7. + F. Guidi: An Efficient Validation Procedure for the Formal System λδ (2010-07). Presentation at CiE 2010 (slides).
+ +
+
+ P6. + F. Guidi: A Validator for the Formal System λδ (revised 2010-02). Presentation at University of Bologna (slides).
+ +
P6.
+
+ V2. + F. Guidi: lambdadelta_2 (revised 2014-07). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry.
+ +
F. -Guidi: A Validator for the Formal System λδ -(revised 2010-02). -Presentation at University of Bologna (slides).
-

[Basic
-                  lambdadelta Logo] Basic λδ version -1 (dismissed):

-The main source of -information is Resource J1. -A summary is found in Resource P5.
-
- + + +
+ [basic lambdadelta] λδ version 1 (dismissed)
+
+ The main source of information is J1. + A summary is available in P5. +
+
+
- - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + +
J1.
+
+ J1. F. -Guidi: The Formal System λδ (2009-11). In ACM ToCL 11(1), pp. -5:1-5:37 (accepted - 2008-07). CoRR -identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.
-
+
F. Guidi: The Formal System λδ (2009-11). In In ACM ToCL 11(1), pp. 5:1-5:37 ( accepted + 2008-07). CoRR identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.
+ +
R3.
+
+ R3. F. -Guidi: Lambda Types on the Lambda Calculus with -Abbreviations (2007-06). - -In - - CiE 2007 Local Proceedings. - -University -of -Siena, technical report 487, p. 387 (abstract of a -presentation). BibTeX entry.
-
+
F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). BibTeX entry.
+ +
R2.
+
+ R2. F. -Guidi: Lambda Types on the Lambda Calculus with -Abbreviations (2006-11). - -University -of -Bologna, technical report UBLCS-2006-25. BibTeX entry.
-
+
F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.
+ +
R1.
+
+ R1. F. -Guidi: Lambda - -Types -on -the Lambda Calculus with Abbreviations: a Certified -Specification (2006-01). -University of Bologna, technical report UBLCS-2006-01. BibTeX entry.
-
+
F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification (2006-01). University of Bologna, technical report UBLCS-2006-01. BibTeX entry.
+ +
P5.
+
+ P5. F. -Guidi: The - -Formal -System - λδ (2008-10). Presentation at "Advances -in Constructive Topology and Logical Foundations" (slides).
-
+
F. Guidi: The Formal System λδ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).
+ +
P4.
+
+ P4. F. -Guidi: Towards the Unification of Terms, Types -and Contexts (2008-03). - -Presentation -at -Types 2008 (slides).
-
+
F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).
+ +
P3.
+
+ P3. F. -Guidi: Lambda Types on the Lambda Calculus with -Abbreviations (2007-06). - -Presentation -at -CiE 2007 (slides).
-
+
F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).
+ +
P2.
+
+ P2. F. -Guidi: Lambda Tipi sul Lambda Calcolo con -Abbreviazioni (2007-01). - -Presentation -at -University of Padova (slides in -Italian).
-
+
F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).
+ +
P1.
+
+ P1. F. -Guidi: Lambda Tipi sul Lambda Calcolo con -Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University -of Bologna (slides in -Italian).
+
F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian).
+ +
-
-
-[Valid HTML 4.01 Transitional] [Use Any
-          Browser Here] [PNG Used Here]
-
-Last update 2014-06-19 by Ferruccio -Guidi
-
+ + +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 20 Jul 2014 11:35:27 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index b4de9bbf6..32705c284 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -234,6 +234,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:32 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index f81968eb6..e6e6a2434 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -31,7 +31,7 @@ - foreword + home news @@ -42,58 +42,42 @@ implementation - -
- - -
-
-
+ Foreword -
+ Milestones -
+ Version 2 Version 2 - + Background - - Core - - Applications - -
+ + Notice - -
+ + Visibility - -
+ + Version 1 Version 1 - -
- - -
-
@@ -202,6 +186,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:32 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 2c1fa2f10..f526a75a9 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -31,7 +31,7 @@ - foreword + home news @@ -42,58 +42,42 @@ implementation - -
- - -
-
-
+ Foreword -
+ Milestones -
+ Version 2 Version 2 - + Background - - Core - - Applications - -
+ + Notice - -
+ + Visibility - -
+ + Version 1 Version 1 - -
- - -
-
@@ -302,6 +286,6 @@

-
Last update: Mon, 14 Jul 2014 22:47:32 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index 9d55641e4..856c396a8 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -31,7 +31,7 @@ - foreword + home news @@ -42,58 +42,42 @@ implementation - -
- - -
-
-
+ Foreword -
+ Milestones -
+ Version 2 Version 2 - + Background - - Core - - Applications - -
+ + Notice - -
+ + Visibility - -
+ + Version 1 Version 1 - -
- - -
-
@@ -185,6 +169,6 @@

-
Last update: Mon, 14 Jul 2014 22:49:03 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index 81cbf0cf5..530f2ad47 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -31,7 +31,7 @@ - foreword + home news @@ -42,58 +42,42 @@ implementation - -
- - -
-
-
+ Foreword -
+ Milestones -
+ Version 2 Version 2 - + Background - - Core - - Applications - -
+ + Notice - -
+ + Visibility - -
+ + Version 1 Version 1 - -
- - -
-
@@ -150,6 +134,6 @@

-
Last update: Mon, 14 Jul 2014 22:49:03 +0200
+
Last update: Sun, 20 Jul 2014 11:29:55 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml new file mode 100644 index 000000000..3e7a6526f --- /dev/null +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -0,0 +1,32 @@ + + + + + + Documentation + + BibTeX database of λδ documentation: + lambdadelta.bib, + lambdadelta.txt + (revised ). + + +
λδ version 2 (in progress)
+ + The main source of information is . + + + +
λδ version 1 (dismissed)
+ + The main source of information is . + A summary is available in . + +
+ +
+ diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl new file mode 100644 index 000000000..fe91832cd --- /dev/null +++ b/helm/www/lambdadelta/web/home/documentation_1.tbl @@ -0,0 +1,91 @@ +name "documentation_1" + +table { + [ { name "ldp5" "J1." "" } { + "F. Guidi:" + + @("http://doi.acm.org/10.1145/1614431.1614436" + "The Formal System λδ") + + "(2009-11)." + + "In In ACM ToCL 11(1), pp. 5:1-5:37 (" + + @("http://tocl.acm.org/accepted/335guidi.pdf" "accepted") + + "2008-07)." + + "CoRR identifier" + + @("http://arxiv.org/abs/cs/0611040" "cs/0611040") + + "[v10] (revised" + + "2008-09)." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldp4" "R3." "" } { + "F. Guidi:" + + @@("download/cie_2007.pdf" + "Lambda Types on the Lambda Calculus with Abbreviations") + + "(2007-06)." + + "In CiE 2007 Local Proceedings." + + "University of Siena, technical report 487, p. 387" + + "(abstract of a presentation)." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldp3" "R2." "" } { + "F. Guidi:" + + @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25" + "Lambda Types on the Lambda Calculus with Abbreviations") + + "(2006-11)." + + "University of Bologna, technical report UBLCS-2006-25." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldp2" "R1." "" } { + "F. Guidi:" + + @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01" + "Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification") + + "(2006-01)." + + "University of Bologna, technical report UBLCS-2006-01." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldt5" "P5." "" } { + "F. Guidi:" + + @@("download/ld_talk_5s.pdf" "The Formal System λδ") + + "(2008-10)." + + "Presentation at Advances in Constructive Topology and Logical Foundations (slides)." + * } + ] + [ { name "ldt4" "P4." "" } { + "F. Guidi:" + + @@("download/ld_talk_4s.pdf" + "Towards the Unification of Terms, Types and Contexts") + + "(2008-03)." + + "Presentation at Types 2008 (slides)." + * } + ] + [ { name "ldt3" "P3." "" } { + "F. Guidi:" + + @@("download/ld_talk_3s.pdf" + "Lambda Types on the Lambda Calculus with Abbreviations") + + "(2007-06)." + + "Presentation at CiE 2007 (slides)." + * } + ] + [ { name "ldt2" "P2." "" } { + "F. Guidi:" + + @@("download/ld_talk_2s.pdf" + "Lambda Tipi sul Lambda Calcolo con Abbreviazioni") + + "(2007-01)." + + "Presentation at University of Padova (slides" + + "in Italian)." + * } + ] + [ { name "ldt1" "P1." "" } { + "F. Guidi:" + + @@("download/ld_talk_1s.pdf" + "Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") + + "(2005-12)." + + "Presentation at University of Bologna (slides" + + "in Italian)." + * } + ] +} + +class "top" [ * ] diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl new file mode 100644 index 000000000..7262f6c81 --- /dev/null +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -0,0 +1,57 @@ +name "documentation_2" + +table { + [ { name "ldp7" "R5." "" } { + "F. Guidi:" + + @@("download/cie_2010.pdf" + "An Efficient Validation Procedure for the Formal System λδ") + + "(2010-07)." + + "In CiE 2010 Local Proceedings." + + "University of Azores, CMATI Booklet, pp. 204-213." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldp6" "R4." "" } { + "F. Guidi:" + + @("http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16" + "Landau's \"Grundlagen der Analysis\" from Automath to lambda-delta") + + "(2009-09)." + + "University of Bologna, technical report UBLCS-2009-16." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] + [ { name "ldt8" "P8." "" } { + "F. Guidi:" + + @@("download/ld_talk_8s.pdf" + "The Formal System λδ and the \"Three Problems\"") + + "(2014-06)." + + "Presentation at University of Bologna (slides)." + * } + ] + [ { name "ldt7" "P7." "" } { + "F. Guidi:" + + @@("download/ld_talk_7s.pdf" + "An Efficient Validation Procedure for the Formal System λδ") + + "(2010-07)." + + "Presentation at CiE 2010 (slides)." + * } + ] + [ { name "ldt6" "P6." "" } { + "F. Guidi:" + + @@("download/ld_talk_6s.pdf" + "A Validator for the Formal System λδ") + + "(revised 2010-02)." + + "Presentation at University of Bologna (slides)." + * } + ] + [ { name "ldV2" "V2." "" } { + "F. Guidi:" + + @@("version_2.html" "lambdadelta_2") + + "(revised 2014-07)." + + "Formal specification for the proof assistant Matita 0.99.2 (scripts)." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] +} + +class "top" [ * ] diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index e29f80dd9..71cc44367 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -2,17 +2,24 @@ name "sitemap" table [ class "sky" { - [ @@("index" "foreword") * ] [ { * } ] + [ @@("index" "home") * ] + [ @@("index#foreword" "Foreword") * ] + [ @@("index#notice" "Notice") * ] } class "magenta" { - [ @@"news" * ] [ { * } ] + [ @@"news" * ] + [ @@("news#milestones" "Milestones") * ] + [ @@("news#visibility" "Visibility") * ] } class "orange" { - [ @@"documentation" * ] [ { * } ] + [ @@"documentation" * ] + [ @@("documentation#v2" "Version 2") * ] + [ @@("documentation#v1" "Version 1") * ] } class "green" { [ @@"implementation" * ] - [ @@("version_2" "Version 2") @@("ground_2" "Background") @@("basic_2" "Core") @@("apps_2" "Applications") * ] + [ @@("version_2" "Version 2") + @@("ground_2" "Background") + @@("basic_2" "Core") + @@("apps_2" "Applications") * ] [ @@("version_1" "Version 1") * ] * } ] -- 2.39.2