From: Ferruccio Guidi Date: Sat, 23 Jan 2016 08:51:34 +0000 (+0000) Subject: documentation update X-Git-Tag: make_still_working~658 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03401922e645207c7b64b52e1c4349f7951fcf71;p=helm.git documentation update --- diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index b3830c1cd..c89fbcf38 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Wed, 30 Dec 2015 15:33:02 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 764ecaa30..45e5d6084 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -124,7 +124,7 @@ J3a. - F. Guidi: Verified Representations of Landau's "Grundlagen" in λδ and in the Calculus of Constructions (2015-08). Submitted to JFR, Univerity of Bologna. BibTeX entry. + F. Guidi: Verified Representations of Landau's "Grundlagen" in the λδ Family and in the Calculus of Constructions (2015-12). In JFR 8(1), Univerity of Bologna, pp. 93-116. BibTeX entry. @@ -389,6 +389,6 @@

-
Last update: Wed, 30 Dec 2015 15:33:02 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index 403c201cd..5e80745cf 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -1,11 +1,16 @@ % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@misc{lambdadeltaJ3a, +@article{lambdadeltaJ3a, author="F. {Guidi}", - title="{Verified Representations of Landau's ``Grundlagen'' in $\lambda\delta$ and in the Calculus of Constructions}", + 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", + journal="Journal of Formalized Reasoning", + volume="8", + number="1", year="2015", - month="August", - note="Submitted to JFR, University of Bologna (available at $<$\url{http://lambdadelta.info/}$>$)" + month="December", + pages="93-116" } % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index 403c201cd..5e80745cf 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -1,11 +1,16 @@ % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@misc{lambdadeltaJ3a, +@article{lambdadeltaJ3a, author="F. {Guidi}", - title="{Verified Representations of Landau's ``Grundlagen'' in $\lambda\delta$ and in the Calculus of Constructions}", + 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", + journal="Journal of Formalized Reasoning", + volume="8", + number="1", year="2015", - month="August", - note="Submitted to JFR, University of Bologna (available at $<$\url{http://lambdadelta.info/}$>$)" + month="December", + pages="93-116" } % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 4e5e6b192..698d60ab5 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -275,6 +275,6 @@

-
Last update: Wed, 30 Dec 2015 15:33:02 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 9272c2a2a..abbd7940a 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -132,29 +132,29 @@ sizes files - 48 + 54 characters - 66783 + nodes - 134126 + 152278 propositions theorems - 9 + 15 lemmas - 298 + 328 total - 307 + 343 concepts declared - 47 + 48 defined - 32 + 39 total - 79 + 87 @@ -213,6 +213,34 @@ multiple relocation + nstream + nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ trace ( ∥?∥ ) trace_at ( @⦃?,?⦄ ≡ ? ) trace_after ( ? ⊚ ? ≡ ? ) @@ -271,12 +299,8 @@ arith ( ?^? ) ( ⫯? ) ( ⫰? ) list ( ◊ ) ( ? @ ? ) ( |?| ) list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) - -
- - -
- + stream ( ? @ ? ) ( ? ≐ ? ) + stream_hdtl generated logical decomposables @@ -359,6 +383,6 @@

-
Last update: Thu, 10 Dec 2015 16:13:46 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 11364dc30..4f198e9fd 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -291,6 +291,6 @@

-
Last update: Wed, 30 Dec 2015 15:33:02 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 5ac10fed3..59973f01f 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -136,7 +136,7 @@ @@ -276,6 +276,6 @@

-
Last update: Wed, 30 Dec 2015 15:33:02 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 13291a901..3d676d294 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -105,6 +105,13 @@
Milestones [spacer]
+ + +
+ [spacer] λδ version 3 (proposed)
+
+ The formal specification of λδ version 3 + is forthcoming. +
[spacer] λδ version 2 (active)
@@ -360,6 +382,6 @@

-
Last update: Wed, 30 Dec 2015 15:33:02 +0100
+
Last update: Sat, 23 Jan 2016 00:45:18 +0100
diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl index cf80e782d..b4dd848a6 100644 --- a/helm/www/lambdadelta/web/home/documentation_3.tbl +++ b/helm/www/lambdadelta/web/home/documentation_3.tbl @@ -3,10 +3,10 @@ name "documentation_3" table { [ { name "ldJ3a" "J3a." "" } { "F. Guidi:" + - @@("download/gda.pdf" - "Verified Representations of Landau's \"Grundlagen\" in λδ and in the Calculus of Constructions") + - "(2015-08)." + - "Submitted to JFR, Univerity of Bologna." + + @("http://jfr.unibo.it/article/view/4716" + "Verified Representations of Landau's \"Grundlagen\" in the λδ Family and in the Calculus of Constructions") + + "(2015-12)." + + "In JFR 8(1), Univerity of Bologna, pp. 93-116." + @@("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 5110c1470..9913b2401 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -41,7 +41,7 @@ C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi: - ELPI: fast, Embeddable, λProlog Interpreter + ELPI: Fast, Embeddable, λProlog Interpreter (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer. diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 966e0fa4c..2e6e14936 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -11,6 +11,11 @@ Milestones + + Second journal paper on λδ + accepted for publication. + + "Helena 0.8.3" is released. diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index a489b47a8..969e3fd00 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -44,6 +44,14 @@ introduced in each script, is shown in parentheses (? are placeholders). + + + λδ version 3 (proposed) + + The formal specification of λδ version 3 + is forthcoming. + + λδ version 2 (active) diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl index 5b7189241..1d88064b3 100644 --- a/helm/www/lambdadelta/web/home/versions.tbl +++ b/helm/www/lambdadelta/web/home/versions.tbl @@ -6,6 +6,11 @@ table { "stage" "started" "announced" "released" "concluded" "references" ] + class "yellow" + [ @@("specification#v3" "Version 3") "\"basic_3\"" "" + "" "" "" "" "" + @@("documentation#ldJ3a" "J3a") + ] class "orange" { [ { @@("specification#v2" "Version 2") * } { "\"basic_2\"" * }