The Formal System λδ (lambda_delta)

Towards the unification of terms, types, environments and contexts

Foreword

News

Papers

Resources

Computer-checked formal specifications

Resource 1 below provides for the statically generated natural language representation of λδ meta-theory (faster rendering w.r.t. resource 2 below).
Resource 2 below provides for the dynamically generated natural language representation of λδ meta-theory (powered by the HELM rendering engine).
Remarkably, λδ was born and developed in the digital format of resource 3 below, which is not the formal counterpart of some informal material previously written on paper (as it happens for most currently digitalized Mathematics).

F. Guidi: lambda_delta (revised 2011-09). Formal specification with the proof assistant Matita 0.5 (HTML pages generated by the HELM rendering engine)
Here are the most relevant theorems proved in the formal specification:
- Confluence of reduction (Church-Rosser property).
- Correctness of types.
- Uniqueness of types up to conversion.
- Subject reduction of the type assignment.
- Strong normalization of the typed terms.
- Decidability of the type inference problem.
F. Guidi: lambda_delta (revised 2011-09). Formal specification with the proof assistant Matita 0.5 (HELM directory).
F. Guidi: lambda_delta_1 (revised 2011-09). Formal specification with the proof assistant Coq 7.3.1 (source proof scripts). BibTeX entry.

Tools

The λδ Digital Library (LDDL) is part of HELM and contains a set of resources expressed in λδ.

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

Access: static pages (updated 2011-09), data set (updated 2011-09), HELM server URL (updated 2011-09).

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

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

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)
- 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. [Svn revision: 10304] (archived source code)
- 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.

Other resources

A BibTeX database of λδ documentation: lambda_delta.bib, lambda_delta.txt (revised 2011-09).

A Jed mode for editing ".hln" files (containing λδ textual syntax): helena.sl (revised 2010-11).

A Jed mode for editing ".aut" files (containing Automath textual syntax): automath.sl (revised 2008-07).

A logo for "basic" λδ: bld.pdf (revised 2008-07).

Last update 2011-09-09 by Ferruccio Guidi