\lambda\delta home page

The Formal System λδ (\lambda\delta)

home	news	documentation	implementation	(specifications - library - Helena)
Foreword	Milestones	Version 2	Version 2	(Background - Core - Applications)
Notice	Visibility	Version 1	Version 1

Computer-checked formal specifications [spacer]

λδ comes in several versions listed in the following 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	July 2014	Planned in 2014	Not planned yet
Version 1	"basic_1"	Coq 7.3.1		May 2004	January 2006	November 2006	May 2008

Tools

λδ Digital Library (LDDL)

The λδ Digital Library is part of HELM and contains resources expressed in λδ.

Contents: Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath).

Access: static pages (updated 2012-10), data set (updated 2012-10), HELM server URL (updated 2012-10).

Examples: Grundlagen's definition "t234" (in "basic_rg" λδ), Grundlagen's definition "t234" (in "complete_rg" λδ).

Helena

Helena is a λδ processor, implemented in Caml as a part of the HELM software, meant for testing the stable features of the calculus as well as the unstable ones.

The processor source code is available in the directory /trunk/helm/software/helena/ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next.

Version 0.8.2. In progress.

Version 0.8.1 (2010-11). Exploits a subset of "complete_rg" λδ as the intermediate language. Features importation from ".hln" files containing λδ textual syntax. The overall validation speed of the "Grundlagen der Analysis" increases of 22% with respect to version 0.8.0. [Svn revision: 11032] (archived source code)
- A Jed mode for editing ".hln" files (containing λδ textual syntax): helena.sl (revised 2010-11).
- 2009-12. Helena appears in F. Wiedijk's index of computer math systems.

Version 0.8.0 (2009-09). Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. Documentation (R4). [Svn revision: 10304] (archived source code).
- A Jed mode for editing ".aut" files (containing Automath textual syntax): automath.sl (revised 2008-07).
- 2009-09. Jutting's specification of Landau's "Grundlagen der Analysis" enters λδ Digital Library.
- 2009-06. Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion.

Last update: Sat, 04 Oct 2014 22:58:58 +0200