applications of \lambda\delta version 2

Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].

@@ -105,30 +171,27 @@

- 2012 February 24. + 2012 February 24. The Applications directory is started.

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

- 2011 December 12. + 2011 December 12. The MLTT1 component is started.

-

Logical Structure of the Specification

-

The source files are grouped in planes and components - according to the following table. - Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). +

Logical Structure of the Specification [spacer]

+

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

@@ -161,10 +224,6 @@

The source files are grouped in directories, - one for each component. -

+ + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ home +	+ news +	+ documentation +	+ specification +	+ +	+ implementation +
+ foreword +	+ milestones +	+ version 2 +	+ version 2 +	(background - core - applications)	+ library +
+ citations +	+ visibility +	+ version 1 +	+ version 1 +	+ +	+ helena +

+

Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].

@@ -60,18 +124,18 @@ - + - + - + - + @@ -86,40 +150,46 @@

files	360	characters	432823	433402	nodes	1874185	1874774
propositions	theorems	130	lemmas	1288	1286	total	1418	1416
concepts

The source files are grouped in planes and components - according to the following table. - Notation files covering the whole specification are provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). +

Logical Structure of the Specification [spacer]

+

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

@@ -515,7 +582,7 @@
- + @@ -641,7 +708,7 @@
- + @@ -879,7 +946,7 @@
- + @@ -893,7 +960,7 @@ - + @@ -921,7 +988,7 @@ - + @@ -1117,7 +1184,7 @@ - + @@ -1158,8 +1225,8 @@ - - + + @@ -1273,10 +1340,6 @@

cpxs ( â¦?,?â¦ â¢ ? â¡*[?,?] ? )

cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs

cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs

cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? )

cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix

cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix

lleq ( ? â¡[?,?] ? )

lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq

lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq

lazy pointwise extension of a relation

llpx_sn

llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor

llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor

context-sensitive exclusion from free variables

frees ( ? â¢ ? Ïµ ð*[?]â¦?â¦ )

frees_append frees_leq frees_lift

frees_append frees_lreq frees_lift

basic local env. slicing

drop ( â¬[?,?,?] ? â¡ ? )

drop_append drop_leq drop_drop

drop_append drop_lreq drop_drop

grammar

equivalence for local environments

leq ( ? â©¬[?,?] ? )

leq_leq

lreq ( ? â©¬[?,?] ? )

lreq_lreq

-

Physical Structure of the Specification

-

The source files are grouped in directories, - one for each component. -

@@ -1303,6 +1366,6 @@

-

Last update: Wed, 22 Oct 2014 20:00:29 +0200

+

Last update: Tue, 28 Oct 2014 17:45:56 +0100

diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index de85f44d0..2b299cf30 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -60,6 +60,11 @@ div.text { font-size: medium; } +span.emph { + font-weight: bold; + font-size: medium; +} + span.date { font-weight: bold; font-size: medium; @@ -106,6 +111,24 @@ img.w3c { height: 32px; /* this should be 31px */ } +/* foreground colors (life cycle) *******************************************/ + +.delta { + color:#500000; +} + +.gamma { + color:#006000; +} + +.beta { + color:#906000; +} + +.alpha { + color:#000000; +} + /* background colors ********************************************************/ .gray { diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 982e13630..51d5ebd97 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -69,10 +69,10 @@ - notice + citations - citations + visibility version 1 @@ -95,26 +95,26 @@

BibTeX database of Î»Î´ documentation: - download + download lambdadelta.bib, - view + view lambdadelta.txt - (revised 2014-10). + (revised 2014-10).

- The main source of information is P8. + The main source of information is P8.

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

- R5. + 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.

@@ -124,9 +124,9 @@

- R4. + 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.

@@ -136,9 +136,9 @@

- P8. + P8.

F. Guidi: The Formal System Î»Î´ and the "Three Problems" (2014-06). Presentation at University of Bologna (slides).

@@ -148,9 +148,9 @@

- P7. + P7.

F. Guidi: An Efficient Validation Procedure for the Formal System Î»Î´ (2010-07). Presentation at CiE 2010 (slides).

@@ -160,9 +160,9 @@

- P6. + P6.

F. Guidi: A Validator for the Formal System Î»Î´ (revised 2010-02). Presentation at University of Bologna (slides).

@@ -172,9 +172,9 @@

- V2. + V2.

F. Guidi: lambdadelta_2 (revised 2014-10). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry.

@@ -187,20 +187,20 @@

-

Î»Î´ version 1 (dismissed)

+

Î»Î´ version 1 (superseded)

- The main source of information is J1. - A summary is available in P5. + 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 ACM ToCL 11(1), pp. 5:1-5:37 (accepted + 2008-07). CoRR identifier cs/0611040 [v10] (revised 2008-09). BibTeX entry.

@@ -210,9 +210,9 @@

- 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.

@@ -222,9 +222,9 @@

- R2. + R2.

F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.

@@ -234,9 +234,9 @@

- 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.

@@ -246,9 +246,9 @@

- P5. + P5.

F. Guidi: The Formal System Î»Î´ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).

@@ -258,9 +258,9 @@

- P4. + P4.

F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).

@@ -270,9 +270,9 @@

- P3. + P3.

F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).

@@ -282,9 +282,9 @@

- P2. + P2.

F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).

@@ -294,9 +294,9 @@

- P1. + P1.

F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian).

@@ -306,9 +306,9 @@

- V1. + V1.

F. Guidi: lambdadelta_1 (revised 2012-10). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry.

@@ -346,6 +346,6 @@

-

Last update: Wed, 22 Oct 2014 20:00:28 +0200

+

Last update: Tue, 28 Oct 2014 17:45:56 +0100

diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index ee6c4e6ee..40e329c0f 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -1,4 +1,4 @@ -% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @misc{lambdadeltaV2, author="F. {Guidi}", @@ -32,7 +32,7 @@ month="September" } -% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{lambdadeltaJ1, author="F. {Guidi}", diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index ee6c4e6ee..40e329c0f 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -1,4 +1,4 @@ -% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @misc{lambdadeltaV2, author="F. {Guidi}", @@ -32,7 +32,7 @@ month="September" } -% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \lambda\delta version 1 (superseded) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{lambdadeltaJ1, author="F. {Guidi}", diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz index de1d12aee..ff9bc8307 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/ground_2.html b/helm/www/lambdadelta/ground_2.html index 49406f8c4..669d0f08f 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -6,8 +6,8 @@ - - background for \lambda\delta version 2 + + \lambda\delta home page @@ -23,13 +23,78 @@

-

Summary of the Specification

+

+
+

+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ home +	+ news +	+ documentation +	+ specification +	+ +	+ implementation +
+ foreword +	+ milestones +	+ version 2 +	+ version 2 +	(background - core - applications)	+ library +
+ citations +	+ visibility +	+ version 1 +	+ version 1 +	+ +	+ helena +

+

+ +

Summary of the Specification [spacer]

+

Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].

@@ -85,28 +150,26 @@

- 2013 November 27. + 2013 November 27. Natural numbers with infinity.

- 2011 August 10. + 2011 August 10. Specification starts.

-

Logical Structure of the Specification

-

The source files are grouped in planes - according to the following table. - Notation files covering the whole specification are provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). +

Logical Structure of the Specification [spacer]

+

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

+ - + + - - + + - - - - - - + + + + + + @@ -175,7 +232,8 @@ - + +

component

plane

files

@@ -135,32 +198,26 @@

natural numbers with infinity

ynat ( â )

ynat_pred ( â«°? )

ynat_succ ( â«¯? )

ynat_le ( ?â¤? )

ynat_lt ( ?<? )

ynat_le ( ? â¤ ? )

ynat_lt ( ? < ? )

ynat_minus ( ? - ? )

ynat_plus ( ? + ? )

ynat_max

ynat_min

extensions to the library

arith.ma ( ?^? )

-
-

extensions to the library

+

star

lstar

bool ( â» ) ( â )

arith ( ?^? )

list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

generated logical decomposables

xoa ( ââ ) ( â¨â¨ ) ( â§â§ )

xoa_props ( â¥ ) ( â¤ )

@@ -204,10 +262,6 @@

-

Physical Structure of the Specification

-

The source files are grouped in directories, - one for each plane. -

@@ -234,6 +288,6 @@

-

Last update: Wed, 22 Oct 2014 20:00:29 +0200

+

Last update: Tue, 28 Oct 2014 17:45:56 +0100

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 7b66a4bb9..6381c533c 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -69,10 +69,10 @@

- notice + citations

- citations + visibility

version 1 @@ -100,24 +100,24 @@ 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), - data set (updated 2012-10), - HELM server URL (updated 2012-10). + Access: + static pages (updated 2012-10), + data set (updated 2012-10), + HELM server URL (updated 2012-10).

- Examples: + Examples: Grundlagen's definition "t234" (in "basic_rg" Î»Î´), @@ -141,15 +141,15 @@ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next. -

- notice + citations

- citations + visibility

version 1 @@ -107,12 +107,10 @@

This is the System logo: crux_177.png - (revised 2012-09). + (revised 2012-09).

- -

Notice for the Internet Explorer user [spacer]

-

+ 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). @@ -120,6 +118,62 @@ "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button.

+ + +

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. +

+

@@ -146,6 +200,6 @@

-

Last update: Wed, 22 Oct 2014 20:00:29 +0200

+

Last update: Tue, 28 Oct 2014 17:45:56 +0100

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index fc49bc3ef..215846e27 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -69,10 +69,10 @@

- notice + citations

- citations + visibility

version 1 @@ -98,21 +98,21 @@

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

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

- December 2012. + December 2012. The character "_" is removed from the denomination "lambda_delta":
- @@ -132,7 +132,7 @@
  - - September 2011. + September 2011. The denomination "lambda-delta" changes to "lambda_delta":
    - @@ -152,7 +152,7 @@
      - - April 2011. + April 2011. The specification of Î»Î´ version 2 and related topics is restarted in Matita 0.5. @@ -161,21 +161,28 @@
        
        - December 2010. + 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. + November 2010. "Helena 0.8.1" is released.
        
        - September 2009. + September 2009. "Helena 0.8.0" is released and the Î»Î´ Digital Library is started. @@ -184,7 +191,7 @@
        
        - June 2009. + June 2009. "Helena", a validator for Î»Î´ version 2, is available as a part of the HELM software.
        @@ -192,14 +199,14 @@
        
        - September 2008. + September 2008. This site is online.
        
        - July 2008. + July 2008. First journal paper on Î»Î´ accepted for publication.
        @@ -207,7 +214,7 @@
        
        - July 2008. + July 2008. First procedural reconstruction for Matita 0.5 of the Î»Î´ version 1 for Coq 7.3.1. @@ -216,7 +223,7 @@
        
        - June 2008. + June 2008. The HTML pages of the specification of Î»Î´ version 1 for Matita 0.5 are online. @@ -225,21 +232,21 @@
        
        - May 2008. - The specification of Î»Î´ version 1 is dismissed. + May 2008. + The specification of Î»Î´ version 1 is concluded.
        
        - March 2008. + March 2008. The specification of Î»Î´ version 2 is started with Coq 7.3.1 (false start).
        
        - September 2007. + September 2007. The specification of Î»Î´ version 1 for Matita 0.4 is online. @@ -248,7 +255,7 @@
        
        - November 2006. + November 2006. Î»Î´ version 1 is released.
        @@ -256,14 +263,14 @@
        
        - December 2005. + December 2005. First communication on Î»Î´ version 1.
        
        - May 2004. + May 2004. The specification of Î»Î´ version 1 is started with Coq 7.3.1.
        @@ -271,68 +278,12 @@ -
        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. -
        -
        - - -
        Visibility
        
        - June 2014. + June 2014. The Google search for "formal system lambda delta" gives 5 resources about Î»Î´ in the first 6 results. @@ -341,7 +292,7 @@
        
        - June 2014. + June 2014. The Yahoo search for "formal system lambda delta" gives 4 resources about Î»Î´ in the first 5 results. @@ -374,6 +325,6 @@
        
        -
        Last update: Wed, 22 Oct 2014 20:00:28 +0200
        +
        Last update: Tue, 28 Oct 2014 17:45:56 +0100
        diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 839278835..bb79c1336 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -69,10 +69,10 @@

- notice + citations

- citations + visibility

version 1 @@ -96,7 +96,20 @@

Î»Î´ is developed as a machine-checked digital specification. It comes in several versions listed in the next table, - which includes the major milestones: + 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, + then the calculus is announced with a presentation. + Beta: + major changes and additions may occur before the calculus is released on paper. + Gamma: + subsequent improvements occur until the specification is completed or superseded, + while major changes and additions are announced and reported on paper. + Delta: + after its conclusion, the specification is modified just for maintenance.

@@ -109,7 +122,7 @@ - + - + + + + + +

started

announced

released

dismissed

concluded

@@ -123,7 +136,19 @@

April 2011

June 2014

October 2014

No

+

Abandoned

+

+ Coq 7.3.1 +

+

March 2008

+

February 2011

@@ -146,7 +171,7 @@

-

Î»Î´ version 2 (ongoing)

+

Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats: @@ -156,14 +181,14 @@

lambdadelta_2 for Matita 0.99.2 - (revised 2014-10). + (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/>. @@ -178,16 +203,23 @@ Applications.

- Notice on numerical acounts: + 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 (dismissed)

+

Î»Î´ version 1 (superseded)

The formal specification of Î»Î´ version 1 is available in the following formats: @@ -197,7 +229,7 @@

lambdadelta_1 for Coq 7.3.1 - (revised 2012-10). + (revised 2012-10). Source scripts.

@@ -209,7 +241,7 @@

lambdadelta_1 for Matita 0.5 - (revised 2011-09). + (revised 2011-09). Static HTML pages generated by the HELM rendering engine.
- @@ -245,9 +277,9 @@
- lambdadelta_1 for Matita 0.5 - (revised 2011-09). + (revised 2011-09). HELM directory. - Notice: the HELM rendering engine is offline. + Notice: the HELM rendering engine is offline.
@@ -277,6 +309,6 @@

-
Last update: Wed, 22 Oct 2014 20:08:56 +0200
+
Last update: Tue, 28 Oct 2014 17:45:56 +0100
diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml index 165dd722f..564307919 100644 --- a/helm/www/lambdadelta/web/home/documentation.ldw.xml +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -10,23 +10,23 @@ Documentation BibTeX database of Î»Î´ documentation: -
+
lambdadelta.bib, -
+
lambdadelta.txt - (revised ). + (revised ). - Î»Î´ version 2 (ongoing) + Î»Î´ version 2 (active) - The main source of information is . + The main source of information is . - Î»Î´ version 1 (dismissed) + Î»Î´ version 1 (superseded) - The main source of information is . - A summary is available in . + 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 index 24fe9ab8f..a12c18683 100644 --- a/helm/www/lambdadelta/web/home/documentation_1.tbl +++ b/helm/www/lambdadelta/web/home/documentation_1.tbl @@ -1,95 +1,95 @@ name "documentation_1" table { - [ { name "ldJ1" "J1." "" } { + [ { name "ldJ1" "J1." "" } { "F. Guidi:" + @("http://doi.acm.org/10.1145/1614431.1614436" "The Formal System Î»Î´") + - "(2009-11)." + + "(2009-11)." + "In ACM ToCL 11(1), pp. 5:1-5:37 (" ^ @("http://tocl.acm.org/accepted/335guidi.pdf" "accepted") + - "2008-07)." + + "2008-07)." + "CoRR identifier" + @("http://arxiv.org/abs/cs/0611040" "cs/0611040") + "[v10] (revised" + - "2008-09)." + + "2008-09)." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR3" "R3." "" } { + [ { name "ldR3" "R3." "" } { "F. Guidi:" + @@("download/cie_2007.pdf" "Lambda Types on the Lambda Calculus with Abbreviations") + - "(2007-06)." + + "(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 "ldR2" "R2." "" } { + [ { name "ldR2" "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)." + + "(2006-11)." + "University of Bologna, technical report UBLCS-2006-25." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR1" "R1." "" } { + [ { name "ldR1" "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)." + + "(2006-01)." + "University of Bologna, technical report UBLCS-2006-01." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldP5" "P5." "" } { + [ { name "ldP5" "P5." "" } { "F. Guidi:" + @@("download/ld_talk_5s.pdf" "The Formal System Î»Î´") + - "(2008-10)." + + "(2008-10)." + "Presentation at Advances in Constructive Topology and Logical Foundations (slides)." * } ] - [ { name "ldP4" "P4." "" } { + [ { name "ldP4" "P4." "" } { "F. Guidi:" + @@("download/ld_talk_4s.pdf" "Towards the Unification of Terms, Types and Contexts") + - "(2008-03)." + + "(2008-03)." + "Presentation at Types 2008 (slides)." * } ] - [ { name "ldP3" "P3." "" } { + [ { name "ldP3" "P3." "" } { "F. Guidi:" + @@("download/ld_talk_3s.pdf" "Lambda Types on the Lambda Calculus with Abbreviations") + - "(2007-06)." + + "(2007-06)." + "Presentation at CiE 2007 (slides)." * } ] - [ { name "ldP2" "P2." "" } { + [ { name "ldP2" "P2." "" } { "F. Guidi:" + @@("download/ld_talk_2s.pdf" "Lambda Tipi sul Lambda Calcolo con Abbreviazioni") + - "(2007-01)." + + "(2007-01)." + "Presentation at University of Padova (slides" + - "in Italian)." + "in Italian)." * } ] - [ { name "ldP1" "P1." "" } { + [ { name "ldP1" "P1." "" } { "F. Guidi:" + @@("download/ld_talk_1s.pdf" "Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") + - "(2005-12)." + + "(2005-12)." + "Presentation at University of Bologna (slides" + - "in Italian)." + "in Italian)." * } ] - [ { name "ldV1" "V1." "" } { + [ { name "ldV1" "V1." "" } { "F. Guidi:" + @@("version_1.html" "lambdadelta_1") + - "(revised 2012-10)." + + "(revised 2012-10)." + "Formal specification for the proof assistant Coq 7.3.1 (scripts)." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 434ebbd64..8d85ec953 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -1,53 +1,53 @@ name "documentation_2" table { - [ { name "ldR5" "R5." "" } { + [ { name "ldR5" "R5." "" } { "F. Guidi:" + @@("download/cie_2010.pdf" "An Efficient Validation Procedure for the Formal System Î»Î´") + - "(2010-07)." + + "(2010-07)." + "In CiE 2010 Local Proceedings." + "University of Azores, CMATI Booklet, pp. 204-213." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR4" "R4." "" } { + [ { name "ldR4" "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)." + + "(2009-09)." + "University of Bologna, technical report UBLCS-2009-16." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldP8" "P8." "" } { + [ { name "ldP8" "P8." "" } { "F. Guidi:" + @@("download/ld_talk_8s.pdf" "The Formal System Î»Î´ and the \"Three Problems\"") + - "(2014-06)." + + "(2014-06)." + "Presentation at University of Bologna (slides)." * } ] - [ { name "ldP7" "P7." "" } { + [ { name "ldP7" "P7." "" } { "F. Guidi:" + @@("download/ld_talk_7s.pdf" "An Efficient Validation Procedure for the Formal System Î»Î´") + - "(2010-07)." + + "(2010-07)." + "Presentation at CiE 2010 (slides)." * } ] - [ { name "ldP6" "P6." "" } { + [ { name "ldP6" "P6." "" } { "F. Guidi:" + @@("download/ld_talk_6s.pdf" "A Validator for the Formal System Î»Î´") + - "(revised 2010-02)." + + "(revised 2010-02)." + "Presentation at University of Bologna (slides)." * } ] - [ { name "ldV2" "V2." "" } { + [ { name "ldV2" "V2." "" } { "F. Guidi:" + @@("version_2.html" "lambdadelta_2") + - "(revised 2014-10)." + + "(revised 2014-10)." + "Formal specification for the proof assistant Matita 0.99.2 (scripts)." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 1c357b3c1..48ff2c594 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -14,23 +14,26 @@ The Î»Î´ Digital Library is part of HELM and contains resources expressed in Î»Î´. - + + Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath). - - - static pages (updated ), - data set (updated ), - HELM server URL (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" Î»Î´). - + Helena @@ -45,10 +48,12 @@ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next. - + + In progress. - - + + + Exploits a subset of "complete_rg" Î»Î´ as the intermediate language. Features importation from ".hln" files containing Î»Î´ textual syntax. The overall validation speed of the "Grundlagen der Analysis" @@ -58,15 +63,16 @@ A Jed mode for editing ".hln" files (containing Î»Î´ textual syntax): helena.sl - (revised ). + (revised ). - + Helena appears in F. Wiedijk's index of computer math systems. - - + + + Supports "basic_rg" Î»Î´ with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. @@ -77,16 +83,16 @@ for editing ".aut" files (containing Automath textual syntax): automath.sl - (revised ). + (revised ). - + Jutting's specification of Landau's "Grundlagen der Analysis" enters Î»Î´ Digital Library. - + Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion. - +
diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index 8517a56ef..e37ac33b2 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -22,11 +22,10 @@ This is the System logo: crux_177.png - (revised ). + (revised ). - - Notice for the Internet Explorer user + 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). @@ -34,5 +33,48 @@ "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button. + + + Citations + + This is a list of publications citing Î»Î´ (not including our own). + + + + A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: + + (2012). In JAR 49(3), pp. 427-451. + + + + M.E. Maietti: + + (2012). Submitted article. + + + + W. Ricciotti: + + (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. + + + + C.E. Brown: + + (2011). Typescript note. + + + + M.E. Maietti: + + (2009). In APAL 160(3), pp. 319-354. + + + + V. Rahili: + + (July 2007). Typescript note. + +
diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index a913b1fc1..6254202c9 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -11,15 +11,15 @@ Milestones - + A new version of this site is online. - + First communication on Î»Î´ version 2. - + The character "_" is removed from the denomination "lambda_delta": The denomination "\lambda\delta" is used in Î»Î´-related texts. @@ -32,7 +32,7 @@ - + The denomination "lambda-delta" changes to "lambda_delta": The character "-" is reserved in Î»Î´ textual syntax @@ -45,134 +45,95 @@ - + The specification of Î»Î´ version 2 and related topics is restarted in Matita 0.5. - + + The specification of Î»Î´ version 2 with Coq 7.3.1 is abandoned. + + + Transient Î»Î´ URL acquired: http://lambda-delta.info/ (expires on December 2012). - + "Helena 0.8.1" is released. - + "Helena 0.8.0" is released and the Î»Î´ Digital Library is started. - + "Helena", a validator for Î»Î´ version 2, is available as a part of the HELM software. - + This site is online. - + First journal paper on Î»Î´ accepted for publication. - + First procedural reconstruction for Matita 0.5 of the Î»Î´ version 1 for Coq 7.3.1. - + The HTML pages of the specification of Î»Î´ version 1 for Matita 0.5 are online. - - The specification of Î»Î´ version 1 is dismissed. + + The specification of Î»Î´ version 1 is concluded. - + The specification of Î»Î´ version 2 is started with Coq 7.3.1 (false start). - + The specification of Î»Î´ version 1 for Matita 0.4 is online. - + Î»Î´ version 1 is released. - + First communication on Î»Î´ version 1. - + The specification of Î»Î´ version 1 is started with Coq 7.3.1. - - - Citations - - This is a list of publications citing Î»Î´ (not including our own). - - - - A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi: - - (2012). In JAR 49(3), pp. 427-451. - - - - M.E. Maietti: - - (2012). Submitted article. - - - - W. Ricciotti: - - (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna. - - - - C.E. Brown: - - (2011). Typescript note. - - - - M.E. Maietti: - - (2009). In APAL 160(3), pp. 319-354. - - - - V. Rahili: - - (July 2007). Typescript note. - - Visibility - + The Google search for "formal system lambda delta" gives 5 resources about Î»Î´ in the first 6 results. - + The Yahoo search for "formal system lambda delta" gives 4 resources about Î»Î´ in the first 5 results. diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index f36c4da24..716f01e69 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -4,12 +4,12 @@ table [ class "sky" { [ @@("index" "home") * ] [ @@("index#foreword" "foreword") * ] - [ @@("index#notice" "notice") * ] + [ @@("index#citations" "citations") * ] } class "magenta" { [ @@"news" * ] [ @@("news#milestones" "milestones") * ] - [ @@("news#citations" "citations") * ] + [ @@("news#visibility" "visibility") * ] } class "orange" { [ @@"documentation" * ] diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index dac9acf84..2bab97a07 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -11,13 +11,26 @@ Î»Î´ is developed as a machine-checked digital specification. It comes in several versions listed in the next table, - which includes the major milestones: + which includes the major milestones. + + + The life cycle of a specification consists of four periods. + + the definitions are designed and the major propositions are proved, + then the calculus is announced with a presentation. + + major changes and additions may occur before the calculus is released on paper. + + subsequent improvements occur until the specification is completed or superseded, + while major changes and additions are announced and reported on paper. + + after its conclusion, the specification is modified just for maintenance.

- Î»Î´ version 2 (ongoing) + Î»Î´ version 2 (active) The formal specification of Î»Î´ version 2 is available in the following formats: @@ -26,14 +39,14 @@ lambdadelta_2 for Matita 0.99.2 - (revised ). + (revised ). Source scripts. The scripts are grouped in directories, first by part, then by component. - + the scripts are checked by the latest version of Matita from HELM Subversion repository at path <trunk/matita/>. @@ -47,15 +60,22 @@ Applications. - + 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]. + + + 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 (dismissed) + Î»Î´ version 1 (superseded) The formal specification of Î»Î´ version 1 is available in the following formats: @@ -64,7 +84,7 @@ lambdadelta_1 for Coq 7.3.1 - (revised ). + (revised ). Source scripts. @@ -74,7 +94,7 @@ lambdadelta_1 for Matita 0.5 - (revised ). + (revised ). Static HTML pages generated by the HELM rendering engine. @@ -101,9 +121,9 @@ lambdadelta_1 for Matita 0.5 - (revised ). + (revised ). HELM directory. - +
diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl index cabffb680..b3cd3e0af 100644 --- a/helm/www/lambdadelta/web/home/versions.tbl +++ b/helm/www/lambdadelta/web/home/versions.tbl @@ -3,11 +3,15 @@ name "versions" table { class "gray" [ "version" "name" "developed with" - "stage" "started" "announced" "released" "dismissed" + "stage" "started" "announced" "released" "concluded" ] class "orange" [ @@("specification#v2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") - "\"A\"" "April 2011" "June 2014" "October 2014" "No" + "\"A\"" "April 2011" "June 2014" "October 2014" "" + ] + class "orange" + [ "Abandoned" "" @("http://coq.inria.fr/" "Coq 7.3.1") + "" "March 2008" "" "" "February 2011" ] class "red" [ @@("specification#v1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1") diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index a6b25cb6f..3d30e6315 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -82,7 +82,7 @@
- +
@@ -120,8 +120,8 @@
- - + +