Computer-checked formal specifications [spacer]

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. @@ -126,7 +132,23 @@ started announced released - concluded + concluded + references + + + + Version 3 + + "basic_3" + + + + + + + + J3a + @@ -136,11 +158,34 @@ Matita 0.99.2 - "A" + "A2" + October 2015 + + + + +
+ + + + +
+ + +
+ + +
+ + "A1" April 2011 June 2014 October 2014 - + August 2015 + + V2a + R2c + Abandoned @@ -152,7 +197,10 @@ March 2008 - February 2011 + February 2011 + +
+ @@ -166,14 +214,45 @@ May 2004 December 2005 November 2006 - May 2008 + May 2008 + + V1a + J1a +

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

Î»Î´ version 2 (active)

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

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

- 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. @@ -201,23 +281,10 @@ 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: @@ -226,8 +293,9 @@

lambdadelta_1 for Coq 7.3.1 - (revised 2015-01). + (revised 2015-09). Source scripts. + Documentation (J1a).

2015 January 15. @@ -283,8 +351,13 @@ 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: Thu, 15 Jan 2015 16:59:16 +0100

Last update: Sat, 16 Apr 2016 14:53:00 +0200