\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
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, then the calculus is announced with a presentation. Beta: major changes and additions may occur before the calculus is released on paper. Gamma: subsequent improvements occur until the specification is completed or superseded, 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

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_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: 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)

The formal specification of λδ version 1 is available in the following formats:

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 (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$

Last update: Thu, 09 Jun 2016 16:46:47 +0200