\lambda\delta home page

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

- home -	- news -	- specification -	- -	- -	- documentation -	- implementation -	- -
- foreword -	- milestones -	- version 2 -	(background - core - applications)	- -	- version 2 -	- helena -	- Open Symbolic Notation (OSN) -
- citations -	- visibility -	- version 1 -	(background - core)	(static HELM directory)	- version 1 -	- library -	(static LDDL directory)

-

+\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

$\lambda\delta rainbow rule$

home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)

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

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, @@ -120,264 +15,71 @@ while major changes and additions are announced and reported on paper. Delta: after its conclusion, the specification is modified just for maintenance. -

-

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

version	name	stage	developed with	started	announced	released	concluded	references
- Version 3 -	"basic_3"	-	-	-	-	-	-	- J3a -
- Version 2 -	"basic_2"	"A2"	- Matita 0.99.3 -	October 2015	-	-	-	-
- -	- -	"A1"	- Matita 0.99.2 -	April 2011	June 2014	October 2014	August 2015	- V2a - R2c -
Abandoned	-	-	- Coq 7.3.1 -	March 2008	-	-	February 2011	-
- Version 1 -	"basic_1"	-	- Coq 7.3.1 -	May 2004	December 2005	November 2006	May 2008	- V1a - J1a -

-

+

version	name	stage	developed with	started	announced	released	concluded	references
Version 3	"basic_3"							J3a
Version 2	"basic_2"	"A2"	Matita 0.99.3	October 2015
		"A1"	Matita 0.99.2	April 2011	June 2014	October 2014	August 2015	V2a R2c
Abandoned			Coq 7.3.1	March 2008			February 2011
Version 1	"basic_1"		Coq 7.3.1	May 2004	December 2005	November 2006	May 2008	V1a J1a

Informational pages on the specifications are provided. -

-

- Notice on displayed numerical acounts: +

+

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

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

- -

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

-

+

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

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

-

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

- -

- $\lambda\delta butterfly$ Î»Î´ 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 +
- lambdadelta_1 for Coq 7.3.1 (revised 2015-09). Source scripts. Documentation (J1a). -
  - - 2015 January 15. +
    - 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. -