[Crux Logo]

The Formal System λδ (lambda_delta)

Towards the unification of terms, types, environments and contexts

[Separator]
  • Resources

Computer-checked formal specifications [Butterfly]

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).
  1. F. Guidi: lambda_delta (revised 2011-09). Formal specification for Matita 0.5 (HTML pages generated by the HELM rendering engine)
    Here are the most relevant theorems proved in the formal specification:
  2. F. Guidi: lambda_delta (revised 2011-09). Formal specification for Matita 0.5 (HELM directory).

  3. F. Guidi: lambda_delta_1 (revised 2011-09). Formal specification for Coq 7.3.1 (source proof scripts). BibTeX entry.

Tools [Butterfly]

[Crux Logo] 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).

[Helena Logo] 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.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)
  • 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 [Butterfly]

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

[Valid HTML 4.01 Transitional] [Use Any
          Browser Here] [PNG Used Here]

Last update 2012-10-16 by Ferruccio Guidi