From: Ferruccio Guidi Date: Fri, 22 Jul 2016 17:12:51 +0000 (+0000) Subject: site update X-Git-Tag: make_still_working~550 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6864d67d5a0e5950a4d5f744866e89215e08ace0;p=helm.git site update --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 32510e3c2..87ca3917c 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index ab26a1c37..e1a4e7961 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -258,6 +258,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 18634b2f7..ad01b3644 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -823,6 +823,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 0a049471c..287810b55 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -144,29 +144,29 @@ sizes files - 154 + 150 characters - 136477 + 128505 nodes - 748562 + 646562 propositions theorems 45 lemmas - 500 + 476 total - 545 + 521 concepts declared 23 defined - 38 + 37 total - 61 + 60 @@ -811,6 +811,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 4de89dc53..fc3e24bc8 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -401,6 +401,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:48 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 6c56317af..e732b224b 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -291,6 +291,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index dc3c8a194..e4ef243ae 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -132,29 +132,29 @@ sizes files - 94 + 92 characters - 129419 + 125262 nodes - 291484 + 265747 propositions theorems - 35 + 33 lemmas - 610 + 588 total - 645 + 621 concepts declared - 61 + 60 defined - 64 + 63 total - 125 + 123 @@ -821,6 +821,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html new file mode 100644 index 000000000..30ed25317 --- /dev/null +++ b/helm/www/lambdadelta/home.html @@ -0,0 +1,288 @@ + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [\lambda\delta home] + +
+
The Formal Systems of the λδ (\lambda\delta) Family
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + helena + + Open Symbolic Notation (OSN) +
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + library + (static LDDL directory)
+
+
Foreword [butterfly] +
+
+ The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support + the foundational frameworks for Mathematics that require an underlying specification language + (for example the Minimalist Foundation + and its predecessors). +
+
+ The λδ family is developed within the + Hypertextual Electronic Library of Mathematics + as a set of machine-checked digital specifications. +
+
+ This is the family logo: crux_177.png + (revised 2012-09). +
+
+ Notice for the user of Internet Explorer. + To view this site correctly, please select a font + with Unicode support. + For example "Lucida Sans Unicode" (it should be already installed on your system). + To change the current font follow: + "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button. +
+ +
Citations [butterfly] +
+
+ This is a list of publications citing λδ documentation. +
+ + + + + + + + +
Disclaimer [butterfly] +
+
+ The systems of the λδ family are not related intentionally to + any other system having (variations of) the symbols λ and δ in its name or syntax. + Examples include (but are not limited to): +
+ + + + + + +
+ [Smiling face] + Moreover, the systems of the λδ family are not related intentionally to + Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. +
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Fri, 22 Jul 2016 19:08:41 +0200
+ + diff --git a/helm/www/lambdadelta/images/b1.png b/helm/www/lambdadelta/images/b1.png new file mode 100644 index 000000000..21d362a10 Binary files /dev/null and b/helm/www/lambdadelta/images/b1.png differ diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 3a681dbe5..dabbb6d2c 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -105,15 +105,15 @@
Tools [butterfly]
- + [Open Symbolic Notation logo] Open Symbolic Notation
Open Symbolic Notation, abbreviated OSN, is an easy and flexible data-interchange text format intended for the lightweight representation of - generic abstract syntax trees in the domain of formal systems. - Additional information will appear soon. + generic abstract syntax trees in the domain of formal languages. + Additional information is available at OSN web site.
[Helena logo] Helena
@@ -302,6 +302,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:48 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html deleted file mode 100644 index abab91aeb..000000000 --- a/helm/www/lambdadelta/index.html +++ /dev/null @@ -1,288 +0,0 @@ - - - - - - - - - - \lambda\delta home page - - - - - - -
- - [\lambda\delta home] - -
-
The Formal Systems of the λδ (\lambda\delta) Family
-
- [Spacer] -
-
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- home - - news - - specification - -
- 		-
- 		- documentation - - implementation - -
-
- foreword - - milestones - - version 2 - (background - core - applications) -
- 		- version 2 - - helena - -
-
- citations - - visibility - - version 1 - (background - core)(static HELM directory) - version 1 - - library - (static LDDL directory)
-
-
Foreword [butterfly] -
-
- The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support - the foundational frameworks for Mathematics that require an underlying specification language - (for example the Minimalist Foundation - and its predecessors). -
-
- The λδ family is developed within the - Hypertextual Electronic Library of Mathematics - as a set of machine-checked digital specifications. -
-
- This is the family logo: crux_177.png - (revised 2012-09). -
-
- Notice for the user of Internet Explorer. - To view this site correctly, please select a font - with Unicode support. - For example "Lucida Sans Unicode" (it should be already installed on your system). - To change the current font follow: - "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button. -
- -
Citations [butterfly] -
-
- This is a list of publications citing λδ documentation. -
- - - - - - - - -
Disclaimer [butterfly] -
-
- The systems of the λδ family are not related intentionally to - any other system having (variations of) the symbols λ and δ in its name or syntax. - Examples include (but are not limited to): -
- - - - - - -
- [Smiling face] - Moreover, the systems of the λδ family are not related intentionally to - Lady Lambdadelta, - the Witch of Certainty of the sound novel - Umineko no Naku Koro ni. -
-
- [Spacer] -
-
-
-
-
- - [Valid XHTML 1.1] - - - [Valid CSS level 2] - - - [Generated from XML via XSL] - - - [PNG used here] - - - [Viewable with any browser] - -
-
-
-
-
Last update: Thu, 21 Jul 2016 16:50:48 +0200
- - diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 711995896..9a7841afe 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -380,6 +380,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:48 +0200
+
Last update: Fri, 22 Jul 2016 19:08:41 +0200
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html index b67c477a3..e367a682d 100644 --- a/helm/www/lambdadelta/osn.html +++ b/helm/www/lambdadelta/osn.html @@ -15,7 +15,7 @@
- + [Open Symbolic Notation logo]
@@ -193,6 +193,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:41 +0200
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index dbf2c18af..f93c67c62 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -378,6 +378,6 @@

-
Last update: Thu, 21 Jul 2016 16:50:49 +0200
+
Last update: Fri, 22 Jul 2016 19:08:42 +0200
diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml new file mode 100644 index 000000000..a7e9b6702 --- /dev/null +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -0,0 +1,156 @@ + + + + + + Foreword + + The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support + the foundational frameworks for Mathematics that require an underlying specification language + (for example the Minimalist Foundation + and its predecessors). + + + The λδ family is developed within the + Hypertextual Electronic Library of Mathematics + as a set of machine-checked digital specifications. + + + This is the family logo: crux_177.png + (revised ). + + + + To view this site correctly, please select a font + with Unicode support. + For example "Lucida Sans Unicode" (it should be already installed on your system). + To change the current font follow: + "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button. + + + + + Citations + + This is a list of publications citing λδ documentation. + + + + C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi: + ELPI: Fast, Embeddable, λProlog Interpreter + (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer. + + + + A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: + Formal metatheory of programming languages in the Matita interactive theorem prover + (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer. + + + + M.E. Maietti: + Consistency of the minimalist foundation with Church thesis and Bar Induction + (2012). Submitted article. + + + + W. Ricciotti: + Theoretical and implementation aspects in the mechanization of the metatheory of programming languages + (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. + + + + C.E. Brown: + Faithful Reproductions of the Automath Landau Formalization + (2011). Technical report. + + + + M.E. Maietti: + A minimalist two-level foundation for constructive mathematics + (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. + + + + V. Rahili: + First Year Report: Realisability methods of proof and semantics with application to expansion + (July 2007). Technical report. + + + + + Disclaimer + + The systems of the λδ family related intentionally to + any other system having (variations of) the symbols λ and δ in its name or syntax. + Examples include (but are not limited to): + + + + λ-δ of + A. Church: + The calculi of lambda-conversion + (1941). + Annals of Mathematics Studies 6. + Princeton University Press. + + + + ∆Λ of + N.G. de Bruijn: + Generalizing Automath by means of a lambda-typed lambda calculus + (1987). + In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92. + Marcel Dekker. + + + + λ∆ of + N.J. Rehof, M.H. Sørensen: + The λ∆-calculus + (1994). + In Lecture Notes in Computer Science, 789, pp. 516–542. + Springer. + + + + λ∆ of + S. Ronchi Della Rocca, L. Paolini: + The Parametric Lambda Calculus + (2004). + Texts in Theoretical Computer Science, An EATCS Series. + Springer. + + + + λD of + R. Nederpelt, H. Geuvers: + Type Theory and Formal Proof + (2014). + Cambridge University Press. + + + + Cλξ of + N.G. de Bruijn: + A namefree lambda calculus with facilities for internal definition of expressions and segments + (1978). + TH-report 78-WSK-03. + Eindhoven University of Technology, Eindhoven. + + + + + Moreover, the systems of the λδ family related intentionally to + Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. + + +