\lambda\delta home page

The Formal System λδ (\lambda\delta)

home	news	documentation	specification		implementation
foreword	milestones	version 2	version 2	(background - core - applications)	library
notice	visibility	version 1	version 1		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:

version	name	developed with	stage	started	announced	released	dismissed
Version 2	"basic_2"	Matita 0.99.2	"A"	April 2011	June 2014	Planned in October 2014	Not planned yet
Version 1	"basic_1"	Coq 7.3.1		May 2004	December 2005	November 2006	May 2008

λδ version 2 (in progress)

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

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

Informational pages on the parts of the specification: Background, Core, Applications.

λδ version 1 (dismissed)

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

lambdadelta_1 for Coq 7.3.1 (revised 2012-10). Source scripts.

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.

Last update: Thu, 09 Oct 2014 16:26:23 +0200