\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	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

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 toversion 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. [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: Sun, 20 Jul 2014 15:02:32 +0200