Computer-checked formal specifications [spacer]

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

The systems of the Î»Î´ family are developed as machine-checked digital specifications, @@ -127,30 +127,43 @@ version name - developed with stage + developed with started announced released concluded references + + + Version 3 + + "basic_3" + + + + + + + + J3a + + Version 2 "basic_2" + "A2" - Matita 0.99.2 + Matita 0.99.3 - "A2" October 2015 - -
- + @@ -159,10 +172,10 @@
- -
- "A1" + + Matita 0.99.2 + April 2011 June 2014 October 2014 @@ -175,27 +188,25 @@ Abandoned + Coq 7.3.1 - March 2008 February 2011 - -
- + Version 1 "basic_1" + Coq 7.3.1 - May 2004 December 2005 November 2006 @@ -228,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$ Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats: @@ -262,7 +280,7 @@

Î»Î´ version 1 (superseded)

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

The formal specification of Î»Î´ version 1 is available in the following formats: @@ -275,7 +293,7 @@ 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