- 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 for Matita 0.5
-(HTML pages generated
-by the HELM
-rendering engine)
-Here are the most relevant theorems proved in the formal specification:
-
- 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)
-
-
2009-12. Helena
-appears in F. Wiedijk's index
+
+
The Formal System λδ (lambda_delta)
+
+
Towards the unification of terms, types, environments and
+ contexts
+ 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 for Matita 0.5
+ (HTML pages generated
+ by the HELM
+ rendering engine)
+ Here are the most relevant theorems proved in the
+ formal specification:
+
+
+ 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.