From: Ferruccio Guidi Date: Thu, 9 Oct 2014 14:39:18 +0000 (+0000) Subject: - update in basic_2 X-Git-Tag: make_still_working~821 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b7395f3e72f7c8db2d81ef8abc8549695c089eca - update in basic_2 - web site major upddate --- diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index b0891996f..fa518c489 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -386,8 +386,8 @@
strongly normalizing qrst-computation - fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? ) - fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? ) + fsb ( ⦥[?,?] ⦃?,?,?⦄ ) + fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ ) fsb_aaa fsb_csx
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index d07a8b977..dd3e6c272 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -40,41 +40,52 @@ documentation + specification + + +
+ + implementation - (specifications - library - Helena) - - Foreword + + foreword - - Milestones + + milestones - - Version 2 + + version 2 - - Version 2 + + version 2 + + (background - core - applications) + + library - (Background - Core - Applications) - - Notice + + notice - - Visibility + + visibility - - Version 1 + + version 1 - - Version 1 + + version 1 - +
+ + helena + @@ -86,11 +97,11 @@ BibTeX database of λδ documentation: lambdadelta.bib, lambdadelta.txt - (revised 2014-07). + (revised 2014-10). -
- [basic lambdadelta logo] λδ version 2 (in progress)
+
+ [spacer] λδ version 2 (in progress)
The main source of information is P8.
@@ -173,8 +184,8 @@ -
- [basic lambdadelta logo] λδ version 1 (dismissed)
+
+ [spacer] λδ version 1 (dismissed)
The main source of information is J1. A summary is available in P5. @@ -333,6 +344,6 @@

-
Last update: Sun, 05 Oct 2014 16:38:32 +0200
+
Last update: Thu, 09 Oct 2014 16:26:23 +0200
diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index 147f0a51a..ee6c4e6ee 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -5,7 +5,7 @@ title="{lambdadelta\_2}", howpublished="Formal specification for the proof assistant Matita 0.99.2", year="2014", - month="July", + month="October", note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" } diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index 147f0a51a..ee6c4e6ee 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -5,7 +5,7 @@ title="{lambdadelta\_2}", howpublished="Formal specification for the proof assistant Matita 0.99.2", year="2014", - month="July", + month="October", note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" } diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz index 74759de60..fd2ae902b 100644 Binary files a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz and b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz differ diff --git a/helm/www/lambdadelta/images/basic_32.png b/helm/www/lambdadelta/images/basic_32.png deleted file mode 100644 index bfbc8634c..000000000 Binary files a/helm/www/lambdadelta/images/basic_32.png and /dev/null differ diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index e0f5b7aab..3d253ae1d 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -40,92 +40,52 @@ documentation + specification + + +
+ + implementation - (specifications - library - Helena) - - Foreword + + foreword - - Milestones + + milestones - - Version 2 + + version 2 - - Version 2 + + version 2 + + (background - core - applications) + + library - (Background - Core - Applications) - - Notice + + notice - - Visibility + + visibility - - Version 1 + + version 1 - - Version 1 + + version 1 - +
- - - -
- -
Computer-checked formal specifications [spacer] -
-
- λδ comes in several versions listed in the following table, - which includes the major milestones: -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
versionnamedeveloped withstagestartedannouncedreleaseddismissed
- Version 2 - "basic_2" - Matita 0.99.2 - "A"April 2011July 2014Planned in 2014Not planned yet
- Version 1 - "basic_1" - Coq 7.3.1 + + helena - May 2004January 2006November 2006May 2008
@@ -134,7 +94,7 @@
Tools [spacer]
-
+
[Crux logo] λδ Digital Library (LDDL)
The λδ Digital Library is part of HELM @@ -167,7 +127,7 @@ -
+
[Helena logo] Helena
Helena is a λδ processor, diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 190bf2ebb..c8664cd96 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -40,41 +40,52 @@ documentation + specification + + +
+ + implementation - (specifications - library - Helena) - - Foreword + + foreword - - Milestones + + milestones - - Version 2 + + version 2 - - Version 2 + + version 2 + + (background - core - applications) + + library - (Background - Core - Applications) - - Notice + + notice - - Visibility + + visibility - - Version 1 + + version 1 - - Version 1 + + version 1 - +
+ + helena + @@ -135,6 +146,6 @@

-
Last update: Sun, 05 Oct 2014 16:38:32 +0200
+
Last update: Thu, 09 Oct 2014 16:26:23 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 1110d7569..c246291df 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -40,41 +40,52 @@ documentation + specification + + +
+ + implementation - (specifications - library - Helena) - - Foreword + + foreword - - Milestones + + milestones - - Version 2 + + version 2 - - Version 2 + + version 2 + + (background - core - applications) + + library - (Background - Core - Applications) - - Notice + + notice - - Visibility + + visibility - - Version 1 + + version 1 - - Version 1 + + version 1 - +
+ + helena + diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html new file mode 100644 index 000000000..568d80fe7 --- /dev/null +++ b/helm/www/lambdadelta/specification.html @@ -0,0 +1,260 @@ + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ (\lambda\delta)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + documentation + + specification + +
+ 		+ implementation +
+ foreword + + milestones + + version 2 + + version 2 + (background - core - applications) + library +
+ notice + + visibility + + version 1 + + version 1 + +
+ 		+ helena +
+
+ +
Computer-checked formal specifications [spacer] +
+
+ λδ is developed as a machine-checked digital specification. + It comes in several versions listed in the next table, + which includes the major milestones: +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
versionnamedeveloped withstagestartedannouncedreleaseddismissed
+ Version 2 + "basic_2" + Matita 0.99.2 + "A"April 2011June 2014Planned in October 2014Not planned yet
+ Version 1 + "basic_1" + Coq 7.3.1 + + May 2004December 2005November 2006May 2008
+
+ + + +
+ [spacer] λδ version 2 (in progress)
+
+ The formal specification of λδ version 2 + is available in the following formats: +
+ + + +
+ Informational pages on the parts of the specification: + Background, + Core, + Applications. +
+ + + +
+ [spacer] λδ version 1 (dismissed)
+
+ The formal specification of λδ version 1 + is available in the following formats: +
+ + + + + + + +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Thu, 09 Oct 2014 16:26:23 +0200
+ + diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index b28827183..40bf6063a 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -167,6 +167,6 @@

-
Last update: Sun, 05 Oct 2014 16:38:32 +0200
+
Last update: Thu, 09 Oct 2014 15:00:23 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index 925508051..b1202c109 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -131,6 +131,6 @@

-
Last update: Sun, 05 Oct 2014 16:38:32 +0200
+
Last update: Thu, 09 Oct 2014 15:00:23 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml index 6dc865edc..338477452 100644 --- a/helm/www/lambdadelta/web/home/documentation.ldw.xml +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -12,16 +12,16 @@ BibTeX database of λδ documentation: lambdadelta.bib, lambdadelta.txt - (revised ). + (revised ). -
λδ version 2 (in progress)
+ λδ version 2 (in progress) The main source of information is . -
λδ version 1 (dismissed)
+ λδ version 1 (dismissed) The main source of information is . A summary is available in . diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 0613d899f..1c357b3c1 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -7,16 +7,9 @@ > - Computer-checked formal specifications - - λδ comes in several versions listed in the following table, - which includes the major milestones: - -
- Tools -
λδ Digital Library (LDDL)
+ λδ Digital Library (LDDL) The λδ Digital Library is part of HELM and contains resources expressed in λδ. @@ -39,7 +32,7 @@ (in "complete_rg" λδ). -
Helena
+ Helena Helena is a λδ processor, implemented in Caml diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 6f9092683..9144fbaf7 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -3,34 +3,37 @@ name "sitemap" table [ class "sky" { [ @@("index" "home") * ] - [ @@("index#foreword" "Foreword") * ] - [ @@("index#notice" "Notice") * ] + [ @@("index#foreword" "foreword") * ] + [ @@("index#notice" "notice") * ] } class "magenta" { [ @@"news" * ] - [ @@("news#milestones" "Milestones") * ] - [ @@("news#visibility" "Visibility") * ] + [ @@("news#milestones" "milestones") * ] + [ @@("news#visibility" "visibility") * ] } class "orange" { [ @@"documentation" * ] - [ @@("documentation#v2" "Version 2") * ] - [ @@("documentation#v1" "Version 1") * ] + [ @@("documentation#v2" "version 2") * ] + [ @@("documentation#v1" "version 1") * ] } class "green" { - [ @@"implementation" - "(" ^ @@("implementation#specifications" "specifications") + "-" + - @@("implementation#lddl" "library") + "-" + - @@("implementation#helena" "Helena") ^ ")" + [ @@"specification" * ] + [ @@("specification#v2" "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") * ] * + [ @@("specification#v1" "version 1") * ] + } + class "green" { + [ @@"implementation" * ] + [ @@("implementation#lddl" "library") * ] + [ @@("implementation#helena" "helena") * ] } ] -class "capitalize italic" [ 0 ] +class "capitalize" [ * ] + +class "italic" [ 0 ] ext ".html" [ * ] diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml new file mode 100644 index 000000000..d32c6ca5d --- /dev/null +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -0,0 +1,88 @@ + + + + + + Computer-checked formal specifications + + λδ is developed as a machine-checked digital specification. + It comes in several versions listed in the next table, + which includes the major milestones: + +
+ + + + λδ version 2 (in progress) + + The formal specification of λδ version 2 + is available in the following formats: + + + + lambdadelta_2 for Matita 0.99.2 + (revised ). + Source scripts. + + + + Informational pages on the parts of the specification: + Background, + Core, + Applications. + + + + + λδ version 1 (dismissed) + + The formal specification of λδ version 1 + is available in the following formats: + + + + lambdadelta_1 for Coq 7.3.1 + (revised ). + Source scripts. + + + + lambdadelta_1 for Matita 0.5" + (revised ). + Static HTML pages generated by the HELM rendering engine. + + + Confluence of reduction + (Church-Rosser property). + + + Correctness of types. + + + Uniqueness of types up to conversion. + + + Subject reduction of the type assignment. + + + Strong normalization of the typed terms. + + + Decidability of the type inference problem. + + + + + + lambdadelta_1 for Matita 0.5" + (revised ). + HELM directory. + + + +
+ diff --git a/helm/www/lambdadelta/web/home/version_1.ldw.xml b/helm/www/lambdadelta/web/home/version_1.ldw.xml deleted file mode 100644 index e80bfe1a7..000000000 --- a/helm/www/lambdadelta/web/home/version_1.ldw.xml +++ /dev/null @@ -1,58 +0,0 @@ - - - - - - Formats - - - The formal specification of λδ version 1 - is available in the following formats: - - - - lambdadelta_1 for Coq 7.3.1 - (revised ). - Source scripts. - - - - lambdadelta_1 for Matita 0.5" - (revised ). - Static HTML pages generated by the HELM rendering engine. - - - Confluence of reduction - (Church-Rosser property). - - - Correctness of types. - - - Uniqueness of types up to conversion. - - - Subject reduction of the type assignment. - - - Strong normalization of the typed terms. - - - Decidability of the type inference problem. - - - - - - lambdadelta_1 for Matita 0.5" - (revised ). - HELM directory. - - - -
- diff --git a/helm/www/lambdadelta/web/home/version_2.ldw.xml b/helm/www/lambdadelta/web/home/version_2.ldw.xml deleted file mode 100644 index 816bface5..000000000 --- a/helm/www/lambdadelta/web/home/version_2.ldw.xml +++ /dev/null @@ -1,31 +0,0 @@ - - - - - - Formats - - - The formal specification of λδ version 2 - is available in the following formats: - - - - lambdadelta_2 for Matita 0.99.2 - (revised ). - Source scripts. - - - - Background, - Core, - Applications. - Informational pages on the parts of the specification. - - -
- diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl index 5c4112e16..49d240c11 100644 --- a/helm/www/lambdadelta/web/home/versions.tbl +++ b/helm/www/lambdadelta/web/home/versions.tbl @@ -4,18 +4,19 @@ table { class "gray" [ "version" "name" "developed with" "stage" "started" "announced" "released" "dismissed" - ] + ] class "orange" - [ @@("version_2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") - "\"A\"" "April 2011" "July 2014" "Planned in 2014" "Not planned yet" - ] + [ @@("specification#v2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") + "\"A\"" "April 2011" "June 2014" "Planned in October 2014" "Not planned yet" + ] class "red" - [ @@("version_1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1") - "" "May 2004" "January 2006" "November 2006" "May 2008" ] + [ @@("specification#v1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1") + "" "May 2004" "December 2005" "November 2006" "May 2008" + ] } class "top" { * } class "capitalize italic" [ 0 ] -ext ".html" { 1 } +ext ".html" { 0 } diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 014d2e65e..a6b25cb6f 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -124,12 +124,17 @@ - - [basic lambdadelta logo] + + + + + + + + + + +