\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

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: Tue, 14 Oct 2014 00:04:55 +0200