\lambda\delta home page

$[\lambda\delta home]$

The Formal Systems of the λδ (\lambda\delta) Family

$\lambda\delta rainbow rule$

home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)

Tools $\lambda\delta butterfly$

Open Symbolic Notation

Open Symbolic Notation, abbreviated OSN, is an easy and flexible data-interchange text format intended for the lightweight representation of generic abstract syntax trees in the domain of formal languages. Additional information is available at OSN web site.

Helena

Helena is a processor for the systems of the λδ family, implemented in Caml as a part of the HELM software, meant for testing both their stable and unstable features.

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.3 (2015-12). Supports exportation to λProlog (two formats for ELPI, and two formats for Teyjus). Employs optimized conditional compilation through camlp5 code preprocessor (pa_macro) to reduce a performance loss, which is expected to disappear by employing a different code preprocessor. Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2: +3% with optimized compilation, +5% without optimized compilation. [Svn revision: 13108] (archived source code).
- 2015-06. The corrected specification of Landau's "Grundlagen der Analysis" is successfully validated in a λProlog implementation of λδ version 3.

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 CC 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.

$[\lambda\delta digital library logo]$ λδ Digital Library (LDDL)

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

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.

$\lambda\delta rainbow rule$

Last update: Thu, 22 Sep 2016 15:52:42 +0200