\lambda\delta home page

The Formal System λδ (\lambda\delta)

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

Computer-checked formal specifications [spacer]

λδ is developed as a machine-checked digital specification. It comes in several versions 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	developed with	stage	started	announced	released	concluded
Version 2	"basic_2"	Matita 0.99.2	"A"	April 2011	June 2014	October 2014
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

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

λδ version 2 (active)

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

lambdadelta_2 for Matita 0.99.2 (revised 2014-10). Source scripts.

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.

λδ version 1 (superseded)

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

lambdadelta_1 for Coq 7.3.1 (revised 2015-01). Source scripts.
- 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: Core.

Last update: Tue, 20 Jan 2015 18:39:00 +0100