@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,15 +62,21 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + +
@@ -74,31 +86,29 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)

- -

Computer-checked formal specifications

Computer-checked formal specifications $\lambda\delta butterfly$

- Î»Î´ is developed as a machine-checked digital specification. - It comes in several versions listed in the next table, - which includes the major milestones. +

+ The systems of the Î»Î´ family are developed as machine-checked digital specifications, + and are 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 +121,7 @@ Delta: after its conclusion, the specification is modified just for maintenance.

@@ -122,7 +132,23 @@ - + + + + + + + - + + + + + + + + + - + @@ -148,7 +197,10 @@ + + - + +

started	announced	released	concluded	concluded	references
+ Version 3 +	"basic_3"	+	+	+	+	+	+	+ J3a +
@@ -132,11 +158,34 @@	Matita 0.99.2	"A"	"A2"	October 2015	+	+	+	+ +
+ +	+ +	+ +	"A1"	April 2011	June 2014	October 2014	+	August 2015	+ V2a + R2c +
Abandoned	March 2008		-	February 2011	February 2011	+ +
@@ -162,129 +214,150 @@	May 2004	December 2005	November 2006	May 2008	May 2008	+ V1a + J1a +

- - - -

Î»Î´ version 2 (active)

+ Informational pages on the specifications are provided. +

+ Notice on displayed 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). +

+ +

+ $\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

+ The formal specification of Î»Î´ version 3 + is forthcoming. +

+ +

+ $\lambda\delta butterfly$ Î»Î´ version 2 (active)

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

- -

-
- lambdadelta_2 for Matita 0.99.2 +
+ lambdadelta_2A1 for Matita 0.99.2 (revised 2014-10). Source scripts. + Documentation (R2c).
-
+
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)

+ +

+ $\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

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

- -

-
- lambdadelta_1 for Coq 7.3.1 - (revised 2012-10). +
+ lambdadelta_1 for Coq 7.3.1 + (revised 2015-09). Source scripts. -
-
+ Documentation (J1a). +
- + 2015 January 15. + 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg". +
+
+
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. -

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

+ $\lambda\delta rainbow rule$

@@ -309,6 +382,6 @@

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

- +

Last update: Thu, 19 May 2016 12:17:40 +0200