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. @@ -128,52 +127,94 @@ 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 + @@ -181,7 +222,7 @@

Informational pages on the specifications are provided.

Notice on displayed numerical acounts: nodes are counted according to the "intrinsic complexity measure" @@ -189,7 +230,7 @@ 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" @@ -198,9 +239,16 @@ 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$

The formal specification of Î»Î´ version 2 is available in the following formats: @@ -208,9 +256,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. @@ -231,7 +280,7 @@

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

The formal specification of Î»Î´ version 1 is available in the following formats: @@ -242,8 +291,9 @@ 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".

2011-09

HELM

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

Core

+ $\lambda\delta rainbow rule$

@@ -328,6 +378,6 @@

Last update: Sun, 11 Oct 2015 17:42:23 +0200

Last update: Fri, 22 Jul 2016 19:34:08 +0200