\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the λδ (\lambda\delta) Family

$\lambda\delta rainbow rule$

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"	"B"	Matita 0.99.4	October 2015	November 2018	November 2019		V2b
		"A"	Matita 0.99.2	April 2011	June 2014	October 2014	August 2015	V2a R2c
Ground	"ground"		Matita 0.99.2	August 2011	March 2016	February 2020
Abandoned			Coq 7.3.1	March 2008			February 2011
Version 1	"basic_1"	"A"	Coq 7.3.1	May 2004	December 2005	November 2006	May 2008	V1a J1a

Change logs: System and Specification (updated 2019-12).

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.

Notice: the scripts are checked by the latest version of Matita from HELM Git repository.

lambdadelta_2B for Matita 0.99.4 (revised 2020-12). Source scripts. Documentation (J2a).
- 2020-12-08. repackaged for publication [Git revision: 2020-12-08 19:00:50].
- 2020-02-27. repackaged without λδ-ground [Git revision: 2020-02-27 22:45:50].
- 2019-11-19. released [Git revision: 2019-11-19 20:45:15].
The scriprs depend on the package lambdadelta_ground.
Informational pages on the parts of the specification: Syntax, Core, Applications.

lambdadelta_2A for Matita 0.99.2 (revised 2020-02). Source scripts. Documentation (R2c).
- 2020-02-27. repackaged on the basis of λδ-ground [Git revision: 2020-02-27 22:45:50].
- 2019-11-20. repackaged (was lambdadelta_2A1) [Git revision: 2019-11-20 19:08:07].
- 2014-10-28. released [Git revision: 2014-10-28 17:46:26].
The scriprs depend on the package lambdadelta_ground.
Informational pages on the parts of the specification: Core.

lambdadelta_ground for Matita 0.99.2 (revised 2020-12). Source scripts.
- 2020-12-08. repackaged for publication [Git revision: 2020-12-08 19:00:50].
- 2020-02-27. released [Git revision: 2020-02-27 22:45:50].
Informational pages on the parts of the specification: Core.

$\lambda\delta butterfly$ λδ version 1 (superseded)

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

lambdadelta_1A for Coq 7.3.1 (revised 2019-11). Source scripts. Documentation (J1a).
- 2019-11-20. repackaging (was lambdadelta_1) [Git revision: 2019-11-20 19:08:07].
- 2015-01-15. 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
Informational pages on the parts of the specification: Background, Core.

lambdadelta_1A for Matita 0.5 (revised 2019-11). 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_1A for Matita 0.5 (revised 2019-11). HELM directory. Notice: the HELM rendering engine is offline.

$\lambda\delta rainbow rule$

Last update: Tue, 22 Dec 2020 18:19:03 +0100

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