\lambda\delta home page

The Formal System λδ (\lambda\delta)

home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	library	(static LDDL directory)
citations	visibility	version 1	(background - core)	(static HELM directory)	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 2015-01), data set (updated 2014-12), HELM server URL (updated 2014-12).

Examples: Grundlagen's definition "t234" in λδ version 4.

Helena

Helena is a processor for λδ, 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 (2015-02). Uses λδ "Version 3" with layer variables as core language. Supports exportation to Gallina (the specification language of Coq), and to Grafite (the specification language of Matita). The overall validation speed of the "Grundlagen der Analysis" increases of 34% with respect to version 0.8.1. Documentation (J3a). [Svn revision: 13035] (archived source code).
- The specification of Landau's "Grundlagen der Analysis" for Coq 8: grundlagen_2.v (revised 2015-02).
- The specification of Landau's "Grundlagen der Analysis" for Matita 0.99.2: grundlagen_2.tar.bz2 (revised 2015-02).
- The corrected specification of Landau's "Grundlagen der Analysis": grundlagen_2.aut (revised 2014-12).
- 2015-02. The translated specification of Landau's "Grundlagen der Analysis" is successfully validated in λC by Coq 8.4.3.
- 2014-12. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in λδ "Version 3".

Version 0.8.1 (2010-11). Uses a subset of λδ "Version 4" as 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 λδ "Version 2" with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. Documentation (R2a). [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: Fri, 07 Aug 2015 14:21:47 +0200