@@ -31,74 +31,84 @@ - home + home news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - - foreword + foreword milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + + Open Symbolic Notation (OSN) - citations + citations 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,180 +121,239 @@ Delta: after its conclusion, the specification is modified just for maintenance.

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

version	name	developed with	stage	developed with	started	announced	released	concluded	concluded	references
+ Version 3 +	"basic_3"	+	+	+	+	+	+	+ J3a +
Version 2	"basic_2"	"A2"	+ Matita 0.99.3 +	October 2015	+	+	+	+
+ +	+ +	"A1"	Matita 0.99.2	"A"	April 2011	June 2014	October 2014	+	August 2015	+ V2a + R2c +
Abandoned	+		Coq 7.3.1		March 2008		-	February 2011	February 2011
Version 1	"basic_1"		Coq 7.3.1		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 +378,6 @@

Last update: Sat, 01 Nov 2014 17:50:21 +0100

- +

Last update: Mon, 06 Mar 2017 23:23:02 +0100