foreword	news	documentation	implementation
			Version 2	Background	Core	Applications
			Version 1

The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support the foundations of Mathematics that require an underlying specification language (for example the Minimal Type Theory and its predecessors).

λδ is developed in the context of the Hypertextual Electronic Library of Mathematics as a machine-checked digital specification that is not the formal counterpart of some previously published informal material.

λδ comes in several versions listed in the following table, which includes the major milestones:

version	name	developed with	started	announced	released	dismissed
2	basic_2	Matita 0.99.2	April 2011	July 2014	Planned in 2014	Not planned yet
1	basic_1	Coq 7.3.1	May 2004	January 2006	November 2006	May 2008

This is the System logo: crux_177.png (revised 2012-09).

To view this site correctly, please select a font with Unicode support. For example "Lucida Sans Unicode" (it should be already installed on your system). To change the current font follow: "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.