Î»Î´ digital library (LDDL)

This table shows how the first 45 positive integers +

Character classes

This table shows how the first 45 positive integers are distributed in the four classes.

@@ -196,8 +196,7 @@

- -

@@ -223,6 +222,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index cbdcfd4f0..f46fcdc30 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -14,8 +14,9 @@ DOWNDIR = download XSLTDIR = xslt XMLDIR = xml SRCDIR = web/home +LDDLDIR = web/lddl XHTBLDIR = bin/xhtbl -HTMLDIR = $(HOME)/public_html/lddl +HTMLDIR = static/lddl JEDDIR = $(HOME)/mps/jed BIBDIR = $(HOME)/texmf/bibtex/bib CONTRIBDIR = $(ETCDIR)/lambdadelta @@ -27,8 +28,8 @@ REMOTE = helm.cs.unibo.it RDIR = /projects/helm/public_html/lambdadelta RHOMEDIR = $(REMOTE):$(RDIR) RXMLDIR = $(RHOMEDIR)/xml -RHTMLDIR = $(RHOMEDIR)/static/lddl RDOWNDIR = $(RHOMEDIR)/download +RHTMLDIR = /projects/helm/public_html/lambda-delta/static SLS = helena.sl automath.sl BIB = lambdadelta.bib @@ -110,8 +111,6 @@ install-xml: $(DOWNDIR)/lddl.tar.bz2 $(H)scp $^ $(RDOWNDIR) $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2" -# $(H)scp -r $(XMLDIR) $(RXMLDIR) - test-html: @$(MAKE) --no-print-directory $(XMLS:%.xml=%) @@ -119,9 +118,11 @@ html: $(ETCDIR)/make_html.sh @echo " MAKE */*.ld" $(H). $< -install-html: $(ETCDIR)/make_html.sh +install-html $(DOWNDIR)/static_lddl.tar.bz2: $(ETCDIR)/exclude.txt $(ETCDIR)/make_html.sh @echo " INSTALL html" - $(H)scp -r $(HTMLDIR)/* $(RHTMLDIR) + $(H)tar -cjf $(DOWNDIR)/static_lddl.tar.bz2 -C static -X $< lddl + $(H)scp $(DOWNDIR)/static_lddl.tar.bz2 $(RDOWNDIR) + $(H)ssh $(REMOTE) "cd $(RHTMLDIR) && tar -xjf ../../lambdadelta/download/static_lddl.tar.bz2 install-jed: $(SLS:%=$(JEDDIR)/%) @echo " INSTALL $(SLS)" @@ -150,10 +151,9 @@ up: %.ld: @echo " XSLT $@" + $(H)mkdir -p $(LDDLDIR)/$(@D) + $(H)$(XSLT) $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml $(H)mkdir -p $(HTMLDIR)/$(@D) - $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml - -%.ldc: - @echo " SKIP $@" + $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml .PHONY: $(TAGS) diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 5184a4d12..9d96b1dbc 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,44 +84,43 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- -

Contents of the Specification

This specification comprises a collection of checked +

This specification comprises a collection of checked applications of Î»Î´ version 2. In particular it contains the components below.

- MLTT1. + MLTT1. Martin-LÃ¶f's Type Theory with one universe using Î»Î´ as theory of expressions.

- Functional. + Functional. The validation algorithm for Î»Î´ as implemented in Helena 0.8.

Summary of the Specification [spacer]

Here is a numerical acount of the specification's contents +

Here is a numerical acount of the specification's contents and its timeline.

@@ -169,31 +172,30 @@

2012 February 24. The Applications directory is started.

2011 December 20. The Functional component is started inside the specification of Î»Î´ version 2.

2011 December 12. The MLTT1 component is started.

Logical Structure of the Specification [spacer]

This table reports the specification's components and their planes. +

This table reports the specification's components and their planes.

@@ -223,8 +225,7 @@

- -

@@ -250,6 +251,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 353b1c74e..a9dd33f1d 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,24 +84,35 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- - -

Summary of the Specification

+ +

Summary of the Specification

Here is a numerical acount of the specification's contents +

Here is a numerical acount of the specification's contents and its timeline.

@@ -149,45 +164,43 @@

- -

Stage "B"

Ongoing. Context-sensitive subject equivalence for native type assignment.

Stage "A": "Extending the Applicability Condition"

2014 October 28. Î»Î´ version 2A is released.

2014 September 9. Iterated static type assignment defined (more elegantly) as a primitive notion.

2014 June 18. Preservation of stratified native validity for context-sensitive computation on terms.

2014 June 9. Strong qrst-normalization for simply typed terms.

2014 April 16. Lazy equivalence on local environments @@ -195,7 +208,7 @@ (anniversary milestone).

2014 January 20. Parametrized slicing of local environments @@ -203,26 +216,26 @@ (one from basic_1, the other used in basic_2 till now).

2013 August 7. Passive support for global environments.

2013 July 27. Reaxiomatized Î²-reductum as in rt-reduction.

2013 July 20. Context-sensitive strong rt-normalization for simply typed terms.

2013 April 16. Reaxiomatized substitution and reduction @@ -230,26 +243,26 @@ (anniversary milestone).

2013 March 16. Mutual recursive preservation of stratified native validity for rst-computation on closures.

2012 October 16. Confluence for context-free parallel reduction on closures.

2012 July 26. Term binders polarized to control Î¶-reduction (not released).

2012 April 16. Context-sensitive subject equivalence @@ -257,43 +270,42 @@ (anniversary milestone).

2012 March 15. Context-sensitive strong normalization for simply typed terms.

2012 January 27. Support for abstract candidates of reducibility.

2011 September 21. Confluence for context-sensitive parallel reduction on terms.

2011 September 6. Confluence for context-free parallel reduction on terms.

2011 April 17. Specification starts.

Logical Structure of the Specification [spacer]

This table reports the specification's components and their planes. +

This table reports the specification's components and their planes.

@@ -1339,8 +1351,7 @@

- -

@@ -1366,6 +1377,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml index 0ff801e93..e60a6a46c 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml @@ -15,6 +15,7 @@ let myself = F.basename (Sys.argv.(0)) let msg = P.sprintf "This file was generated by %s, do not edit" myself let compose uri ext = + if uri.[pred (S.length uri)] = '/' then uri else try let i = S.index uri '#' in let uri, fragment = S.sub uri 0 i, S.sub uri i (S.length uri - i) in diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index 2b299cf30..e5df659b0 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -10,10 +10,13 @@ body { a:link, a:visited, a:hover, a:active, a:focus { text-decoration: underline; - color: rgb(0, 0, 0); + color: inherit; + backgroud: inherit; } a:hover { + text-decoration: underline; + color: inherit; background: rgb(192, 192, 192); } diff --git a/helm/www/lambdadelta/css/lddl.css b/helm/www/lambdadelta/css/lddl.css index 41a635d45..dbcb6c81f 100644 --- a/helm/www/lambdadelta/css/lddl.css +++ b/helm/www/lambdadelta/css/lddl.css @@ -32,6 +32,11 @@ color: rgb(255, 0, 0); } +.proj { + background: rgb(255, 255, 255); + color: rgb(192, 120, 0); +} + .local { background: rgb(255, 255, 255); color: rgb(0, 160, 0); @@ -39,5 +44,5 @@ .global { background: rgb(255, 255, 255); - color: rgb(0, 0, 0); + color: rgb(0, 0, 255); } diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 8d7d6b753..78777483e 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,20 +84,20 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- -

Documentation

BibTeX database of Î»Î´ documentation: download lambdadelta.bib, @@ -101,13 +105,12 @@ lambdadelta.txt (revised 2014-10).

- -

Î»Î´ version 2 (active)

The main source of information is J2.

@@ -197,14 +200,13 @@

- -

Î»Î´ version 1 (superseded)

The main source of information is J1. A summary is available in P5.

@@ -331,8 +333,7 @@

- -

@@ -358,6 +359,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/download/helena_0.8.2.tar.gz b/helm/www/lambdadelta/download/helena_0.8.2.tar.gz new file mode 100644 index 000000000..a184d5b3e Binary files /dev/null and b/helm/www/lambdadelta/download/helena_0.8.2.tar.gz differ diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 7f5ada5fd..b733264ec 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,23 +84,23 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- -

Summary of the Specification

Here is a numerical acount of the specification's contents +

Here is a numerical acount of the specification's contents and its timeline.

@@ -148,24 +152,23 @@

2013 November 27. Natural numbers with infinity.

2011 August 10. Specification starts.

Logical Structure of the Specification [spacer]

This table reports the specification's components and their planes. +

This table reports the specification's components and their planes.

@@ -261,8 +264,7 @@

- -

@@ -288,6 +290,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 5faac4d4c..c50d125e5 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,71 +84,71 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- -

Tools

- -

Î»Î´ Digital Library (LDDL)

The Î»Î´ Digital Library is part of HELM and contains resources expressed in Î»Î´.

- Contents: + Contents: Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath).

- Access: - static pages (updated 2012-10), + Access: + static pages (updated 2015-01), data set (updated 2014-12), HELM server URL (updated 2014-12).

- Examples: - + Examples: + Grundlagen's definition "t234" - (in "basic_rg" Î»Î´), - - Grundlagen's definition "t234" - (in "complete_rg" Î»Î´). + in Î»Î´ version 4.

Helena

- Helena is a Î»Î´ processor, +

+ Helena is a processor for Î»Î´, implemented in Caml as a part of the HELM software, meant for testing the stable features of the calculus as well as the unstable ones.

The processor source code is available in the directory /trunk/helm/software/helena/ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next.

- Version 0.8.2. - In progress. + Version 0.8.2 (2014-12). + Uses Î»Î´ "Version 3" with layer variables as core language. + Supports exportation to Grafite + (the specification language of Matita). + The overall validation speed of the "Grundlagen der Analysis" + increases of 34% with respect to version 0.8.1. + [Svn revision: 13005] (archived source code)
- The specification of Landau's "Grundlagen der Analysis" @@ -158,17 +162,17 @@ (revised 2014-12).
- - 2014-12. + 2014-12. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in Î»Î´ "Version 3".
-

- Version 0.8.1 (2010-11). - Uses a subset of Î»Î´ "Version 4" as the intermediate language. + Version 0.8.1 (2010-11). + Uses a subset of Î»Î´ "Version 4" as intermediate language. Features importation from ".hln" files containing Î»Î´ textual syntax. The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. @@ -181,17 +185,17 @@ (revised 2010-11).
- 2009-12. + 2009-12. Helena appears in F. Wiedijk's index of computer math systems.

- Version 0.8.0 (2009-09). + Version 0.8.0 (2009-09). Supports Î»Î´ "Version 2" with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. @@ -206,19 +210,19 @@ (revised 2008-07).
- 2009-09. + 2009-09. Jutting's specification of Landau's "Grundlagen der Analysis" enters Î»Î´ Digital Library.
- 2009-06. + 2009-06. Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion.

@@ -244,6 +248,6 @@

Last update: Fri, 26 Dec 2014 16:35:05 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 07297ff24..5e923dda1 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,36 +84,36 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- -

Foreword

The formal system Î»Î´ (\lambda\delta) is a typed Î»-calculus aiming to support the foundations of Mathematics that require an underlying specification language (for example the Minimal Type Theory and its predecessors).

Î»Î´ is developed in the context of the Hypertextual Electronic Library of Mathematics as a machine-checked digital specification that is not the formal counterpart of previous informal material.

This is the System 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. @@ -117,64 +121,55 @@ To change the current font follow: "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button.

- - - -

Citations

+ +

Citations

This is a list of publications citing Î»Î´ (not including our own).

- -

A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: Formal metatheory of programming languages in the Matita interactive theorem prover (2012). In JAR 49(3), pp. 427-451.

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). Typescript note.

M.E. Maietti: A minimalist two-level foundation for constructive mathematics (2009). In APAL 160(3), pp. 319-354.

V. Rahili: First Year Report: Realisability methods of proof and semantics with application to expansion (July 2007). Typescript note.

@@ -200,6 +195,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 110c880fb..f9bc87d37 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,37 +84,52 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- - - -

Milestones

+ +

Milestones

- -

+ December 2014. + "Helena 0.8.2" is released. +
- + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in Î»Î´ version 3. +
+

+ October 2014. + Î»Î´ version 2A + is released. +

July 2014. A new version of this site is online.

June 2014. - First communication on Î»Î´ version 2. -

First communication on Î»Î´ version 2.

December 2012. The character "_" is removed from the denomination "lambda_delta": @@ -127,10 +146,9 @@ (pointing at this site).

September 2011. The denomination "lambda-delta" changes to "lambda_delta": @@ -147,10 +165,9 @@ In particular, this refactoring involves file names and path names.

April 2011. The specification of Î»Î´ version 2 @@ -158,61 +175,52 @@ Matita 0.5.

February 2011. The specification of Î»Î´ version 2 with Coq 7.3.1 is abandoned.

December 2010. Transient Î»Î´ URL acquired: http://lambda-delta.info/ (expires on December 2012).

November 2010. - "Helena 0.8.1" is released. + "Helena 0.8.1" is released.

September 2009. - "Helena 0.8.0" is released and the - Î»Î´ Digital Library - is started. + "Helena 0.8.0" is released and the + Î»Î´ Digital Library is started.

June 2009. "Helena", a validator for Î»Î´ version 2, is available as a part of the HELM software.

September 2008. This site is online.

July 2008. - First journal paper on Î»Î´ + First journal paper on Î»Î´ accepted for publication.

July 2008. First procedural reconstruction @@ -220,8 +228,7 @@ of the Î»Î´ version 1 for Coq 7.3.1.

June 2008. The @@ -229,22 +236,19 @@ are online.

- -

May 2008. The specification of Î»Î´ version 1 is concluded.

- -

March 2008. The specification of Î»Î´ version 2 is started with Coq 7.3.1 (false start).

- -

September 2007. The @@ -252,36 +256,30 @@ is online.

- -

November 2006. - Î»Î´ version 1 + Î»Î´ version 1 is released.

December 2005. - First communication on Î»Î´ version 1. + First communication on Î»Î´ version 1.

May 2004. The specification of Î»Î´ version 1 is started with Coq 7.3.1.

Visibility [spacer]

+ +

Visibility [spacer]

- -

June 2014. The Google @@ -289,8 +287,7 @@ 5 resources about Î»Î´ in the first 6 results.

June 2014. The Yahoo @@ -298,8 +295,7 @@ 4 resources about Î»Î´ in the first 5 results.

@@ -325,6 +321,6 @@

Last update: Wed, 24 Dec 2014 22:58:51 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 857add671..72bfee5ba 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -23,7 +23,7 @@

@@ -45,9 +45,12 @@
- + implementation + +
+ @@ -63,9 +66,10 @@ version 2 (background - core - applications) - + library + (static LDDL directory) @@ -80,25 +84,25 @@ version 1 - -
- - + (static HELM directory) + helena + +
+

- -

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.

The life cycle of a specification consists of four periods. Alpha: the definitions are designed and the major propositions are proved, @@ -111,7 +115,7 @@ Delta: after its conclusion, the specification is modified just for maintenance.

@@ -167,123 +171,113 @@

- - - -

+ +

Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats:

- -

-
- lambdadelta_2 for Matita 0.99.2 +
+ lambdadelta_2 for Matita 0.99.2 (revised 2014-10). Source scripts.
-
+
The scripts are grouped in directories, first by part, then by component.
-
- Notice: +
+ Notice: the scripts are checked by the latest version of Matita from HELM Subversion repository at path <trunk/matita/>.
-

Informational pages on the parts of the specification: Background, Core, Applications.

Notice on numerical acounts: nodes are counted according to the "intrinsic complexity measure" [F. Guidi: "Procedural Representation of CIC Proof Terms" Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].

Notice on displayed logical structures: from the logical standpoint, the source scripts are grouped in "planes" and these are grouped in "components"; the notation for the relations or functions introduced in each script, is shown in parentheses (? are placeholders).

- - - -

+ +

Î»Î´ version 1 (superseded)

The formal specification of Î»Î´ version 1 is available in the following formats:

- -

-
- lambdadelta_1 for Coq 7.3.1 +
+ lambdadelta_1 for Coq 7.3.1 (revised 2012-10). Source scripts. -
-
+
+
The scripts are grouped in directories, one for each part.
-

- lambdadelta_1 for Matita 0.5 + lambdadelta_1 for Matita 0.5 (revised 2011-09). 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 2011-09). HELM directory. Notice: the HELM rendering engine is offline. -

@@ -309,6 +303,6 @@

Last update: Wed, 24 Dec 2014 22:58:52 +0100

- +

Last update: Mon, 05 Jan 2015 00:32:03 +0100

+ diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index fdc0ddba1..1d2ffdc96 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -21,23 +21,20 @@ - static pages (updated ), + static pages (updated ), data set (updated ), HELM server URL (updated ). - + Grundlagen's definition "t234" - (in "basic_rg" Î»Î´), - - Grundlagen's definition "t234" - (in "complete_rg" Î»Î´). + in Î»Î´ version 4.

Helena

- Helena is a Î»Î´ processor, + Helena is a processor for Î»Î´, implemented in Caml as a part of the HELM software, meant for testing the stable features of the calculus as well as the unstable ones. @@ -49,8 +46,13 @@ The Svn revisions containing the stable versions of Helena are indicated next. - - In progress. + + Uses Î»Î´ "Version 3" with layer variables as core language. + Supports exportation to Grafite + (the specification language of Matita). + The overall validation speed of the "Grundlagen der Analysis" + increases of 34% with respect to version 0.8.1. + [Svn revision: 13005] (archived source code) The specification of Landau's "Grundlagen der Analysis" for Matita 0.99.2: @@ -68,7 +70,7 @@ - Uses a subset of Î»Î´ "Version 4" as the intermediate language. + Uses a subset of Î»Î´ "Version 4" as intermediate language. Features importation from ".hln" files containing Î»Î´ textual syntax. The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 6254202c9..9f1f7f43e 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -11,6 +11,19 @@ Milestones + + "Helena 0.8.2" is released. + + The corrected specification of Landau's "Grundlagen der Analysis" + is validated in Î»Î´ version 3. + + + + + Î»Î´ version 2A + is released. + + A new version of this site is online. @@ -60,13 +73,12 @@ - "Helena 0.8.1" is released. + "Helena 0.8.1" is released. - "Helena 0.8.0" is released and the - Î»Î´ Digital Library - is started. + "Helena 0.8.0" is released and the + Î»Î´ Digital Library is started. diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 716f01e69..091a90a73 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -23,11 +23,15 @@ table [ @@("basic_2" "core") + "-" + @@("apps_2" "applications") ^ ")" * ] - [ @@("specification#v1" "version 1") * ] + [ @@("specification#v1" "version 1") + "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")" + * ] } class "green" { [ @@"implementation" * ] - [ @@("implementation#lddl" "library") * ] + [ @@("implementation#lddl" "library") + "(" ^ @@("static/lddl/" "static LDDL directory") ^ ")" + * ] [ @@("implementation#helena" "helena") * ] } ] diff --git a/helm/www/lambdadelta/xslt/ld_web.xsl b/helm/www/lambdadelta/xslt/ld_web.xsl index dd091dcd3..c5dc6b449 100644 --- a/helm/www/lambdadelta/xslt/ld_web.xsl +++ b/helm/www/lambdadelta/xslt/ld_web.xsl @@ -7,6 +7,8 @@ + + @@ -16,7 +18,6 @@ doctype-public="-//W3C//DTD XHTML 1.1//EN" doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd" encoding="UTF-8" - indent="yes" /> diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 3d30e6315..8c2c3ad39 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -206,4 +206,10 @@ + + + + + + diff --git a/helm/www/lambdadelta/xslt/lddl.xsl b/helm/www/lambdadelta/xslt/lddl.xsl index 2711cff96..6fd5a3dbf 100644 --- a/helm/www/lambdadelta/xslt/lddl.xsl +++ b/helm/www/lambdadelta/xslt/lddl.xsl @@ -11,23 +11,18 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ --> - + - + - + diff --git a/helm/www/lambdadelta/xslt/lddl_constant.xsl b/helm/www/lambdadelta/xslt/lddl_constant.xsl new file mode 100644 index 000000000..2767eab47 --- /dev/null +++ b/helm/www/lambdadelta/xslt/lddl_constant.xsl @@ -0,0 +1,55 @@ + + + + + + + + + Constant + + + + + + + + + + + + + + + + + + + + + + + + Declaration + + + + + + Definition + + + + diff --git a/helm/www/lambdadelta/xslt/lddl_entity.xsl b/helm/www/lambdadelta/xslt/lddl_entity.xsl deleted file mode 100644 index 9145173e8..000000000 --- a/helm/www/lambdadelta/xslt/lddl_entity.xsl +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - - - - - -

- - - - - - - - - - - - - - -

- - - - -

- -

- - - - - Declaration - - - - - - Definition - - - - diff --git a/helm/www/lambdadelta/xslt/lddl_library.xsl b/helm/www/lambdadelta/xslt/lddl_library.xsl index ccd977990..a126c9ba4 100644 --- a/helm/www/lambdadelta/xslt/lddl_library.xsl +++ b/helm/www/lambdadelta/xslt/lddl_library.xsl @@ -12,26 +12,18 @@ V_______________________________________________________________ --> - - , - - / - - + - - . @@ -52,6 +44,14 @@ ] + + { + + + + } + + < @@ -60,6 +60,10 @@ > + + _ + + : @@ -68,196 +72,72 @@ = - - " + + â - - Informal description: + + Î» - - Validation parameters: + + Î - - sort hierarchy = + + â - - kernel options = + + Î´ - - - - + + Ï - - - - - Π - - - - Π - - - λ - - - λ - ^∞ - - - λ - - - - + + , - - - δ - + + " - - - χ - + + Informal description: - - - - - - - - - - - + + Validation parameters: - - - + + sort hierarchy = - - - - - .html - -

+ + kernel options = - +

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - +

@@ -277,13 +157,119 @@ - + + + + + + + + + + + + .html + +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - λδ Digital Library (LDDL) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/www/lambdadelta/xslt/lddl_root.xsl b/helm/www/lambdadelta/xslt/lddl_root.xsl index f366f6dc4..5645dc7e8 100644 --- a/helm/www/lambdadelta/xslt/lddl_root.xsl +++ b/helm/www/lambdadelta/xslt/lddl_root.xsl @@ -13,90 +13,23 @@ - - - - - - - - - Î»Î´ digital library (LDDL) - - - - -

- -

- -

- -

- -

- -

- -

- + + + + + - - -

+ + +

@@ -108,7 +41,13 @@

+ + + + + + + diff --git a/helm/www/lambdadelta/xslt/lddl_term.xsl b/helm/www/lambdadelta/xslt/lddl_term.xsl index 01ccff3bb..dd5a45083 100644 --- a/helm/www/lambdadelta/xslt/lddl_term.xsl +++ b/helm/www/lambdadelta/xslt/lddl_term.xsl @@ -13,84 +13,86 @@ - - - - - - - - - - - + + + - - - + + + - +

+ - +

- +

+ - +

- + +

+ + + + + + + + + +

- - - - - - - - + + + + + + + +

- - + +

- +