+
+

The Formal System Î»Î´ (lambda-delta)
+

Towards the unification of terms, types, environments and contexts

+ + + + + + + +

Foreword

News

Papers

Resources
+

Documentation

+Currently the main source of +information on Î»Î´ (version 1) is Resource +1.1 below.
+A summary of basic Î»Î´ (version +1) is found in Resource 1.5 +below.
+

Basic Î»Î´ version 2:

+ + + + + + + + + + + + + + + + + + + +

2.1. +	F. Guidi: An +Efficient +Validation Procedure for the Formal System Î»Î´ +(2010-07). In CiE 2010 Local Proceedings. +University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry. + +
2.2. +	F. +Guidi: + + + + + + + + + Landau's +"Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of +Bologna, technical report UBLCS-2009-16. BibTeX entry. + +
2.3. +	F. Guidi: An +Efficient +Validation Procedure for the Formal System Î»Î´ (2010-07). Presentation +at +CiE +2010 +(slides). + +
2.4. +	F. Guidi: A +Validator +for the Formal System Î»Î´ (revised 2010-02). Presentation +at +the +University +of +Bologna +(slides).

Basic Î»Î´ version 1:

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

1.1. +	F. +Guidi: The Formal System Î»Î´ (2009-10). In ACM ToCL 11(1), Article +No. 5 (accepted + 2008-07). CoRR +identifier cs/0611040 [v10] (revised 2008-09). BibTeX +entry. + +
1.2. +	F. Guidi: Lambda Types on the Lambda Calculus with +Abbreviations (2007-06). +In + + + + + + + + + + + + + CiE 2007 Local Proceedings. +University +of +Siena, +technical +report +487, +p. +387 +(abstract +of +a +presentation). + + + + + + + BibTeX +entry. + +
1.3. +	F. Guidi: Lambda Types on the Lambda Calculus with +Abbreviations (2006-11). +University +of +Bologna, +technical +report +UBLCS-2006-25. + + + + + + + + + + + + + + BibTeX +entry. + +
1.4. +	F. Guidi: Lambda +Types +on +the +Lambda +Calculus +with +Abbreviations: +a +Certified +Specification (2006-01). +University of +Bologna, technical report UBLCS-2006-01. BibTeX entry. + +
1.5. +	F. Guidi: The +Formal +System lambda-delta +(2008-10). Presentation at +"Advances in Constructive Topology and Logical Foundations" (slides). + +
1.6. +	F. Guidi: Towards the Unification of Terms, Types +and Contexts (2008-03). +Presentation +at +Types +2008 +(slides). + +
1.7. +	F. Guidi: Lambda Types on the Lambda Calculus with +Abbreviations (2007-06). +Presentation +at +CiE +2007 +(slides). + +
1.8. +	F. Guidi: Lambda Tipi sul Lambda Calcolo con +Abbreviazioni (2007-01). +Presentation +at +the +University +of +Padova +(slides + + + + + + + in +Italian). + +
1.9. +	F. +Guidi: Lambda Tipi sul Lambda Calcolo con +Abbreviazioni: una Specifica Certificata (2005-12). Presentation at +the University of Bologna (slides in +Italian). +

+
+

+
+Last update 2010-12-14 by Ferruccio +Guidi
+

+
+ +
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-TYPES +(revised 2008-06). 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-TYPES +(revised 2008-06). Formal +specification with the proof assistant Matita 0.5 (HELM directory).
+
+
+
F. Guidi: LAMBDA-TYPES (revised 2008-03). +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 2010-11), data set (updated 2010-11), HELM server URL +(updated 2010-11).
+
+
+
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/lambda-delta/ +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 2010-07).
+
+
+
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 2010-12-14 by Ferruccio +Guidi
+

+
+

The Formal System Î»Î´ (lambda-delta)
+

Towards the unification of terms, types, environments and contexts

+ + + + + + + +

Foreword

News

Papers

Resources
+

Foreword

+The formal system Î»Î´ +(lambda-delta) is a typed lambda calculus that pursues the static and +dynamic unification of terms, types, environments and contexts while +enjoying a well-conceived meta-theory, which includes the commonly +desired properties.
+
+Î»Î´ takes some features from the calculi of the Automath family and +some from the pure type systems, but it differs from both in that it +does not include the Î construction while it provides for an +abbreviation mechanism at the level of terms.
+
+Î»Î´ features explicit type annotations, which are borrowed from +realistic type checker implementations and with which type checking is +reduced to type inference.
+
+The reduction steps of Î»Î´ include Î²-contraction, Î´-expansion, +Î¶-contraction and Î¸-swap. On the other hand, +Î·-contraction is not included.
+
+The meta-theory of Î»Î´ includes important properties such as the +confluence of reduction, the correctness of types, the +uniqueness of types up to conversion, the subject reduction of the type +assignment, the strong normalization of the typed terms. The +decidability of type inference and of type checking come as corollaries.
+
+Î»Î´ features uniformly dependent types and a predicative abstraction +mechanism, so the calculus can serve as a formal specification language +for the type theories that need a predicative foundation. Î»Î´ is +expected to have the expressive power of Î»â.
+

Notice +for +the +Internet +Explorer +user

+To view this site +correctly, please select a font with Unicode +support.
+For example Lucida Sans Unicode +(it should be already installed on your system).
+To change the current font follow:
+ "Tools" menu â "Internet +Options" entry â "General" tab â "Fonts" button.
+

+
+

+
+Last update 2010-12-14 by Ferruccio +Guidi
+

+
+

The Formal System Î»Î´ (lambda-delta)
+

Towards the unification of terms, types, environments and contexts

+ + + + + + + +

Foreword

News

Papers

Resources
+

News

December 2010. +Permanent Î»Î´ URL acquired: http://lambda-delta.info +(pointing at this site).
+

November 2010. Helena 0.8.1 is released.
+

September 2009. Helena 0.8.0 is released and the Î»Î´ Digital Library is +started.
+

June 2009. Helena, A validator for Î»Î´, is +available +as a +part of the HELM software.
+

+ +

September 2008. +This site is online.
+

+ +

July 2008. First journal paper on Î»Î´ accepted +for publication.

July 2008. First procedural +reconstruction in Matita 0.5 +of the Î»Î´ proof scripts in +Coq 7.3.1.
+

June 2008. The HTML +pages of the specification of Î»Î´ in Matita 0.5 are online.
+

March 2008. An +improvement of the +specification of Î»Î´ in Coq 7.3.1 begins: +
- native type assignment with new rules for application: nty (it replaces ty3);
  +
- parallel conversion on focalized terms: fpcs (it replaces pc3); + + + + + + + +
  +
- new weak parallel reduction on environments: wcpr (it is based on fpr and replaces wcpr0);
  +
- parallel reduction on focalized terms: fpr and fprs (they replace pr2, pr3);
  +
+
- new thinning relation: drop +(it replaces the old drop, clear, getl, cimp, drop1);
- new shift function: shift: +(it +replaces + app1);
- new length function for environments: clen;
  +
- new relocation function: lift (it replaces old lift, lift1);
  +
- new term structure with polarity indicators and no +distinction between binding and flat items;
- new general theory of relocation (comprises new +relocation functions: s, r);
- we removed context-free reduction and conversion (pr0, pr1, pc1);
  +
- we removed greedy substitution (csubst0, + + + csubst1, fsubst0, subst0, subst1);
  +
- we removed level indicators on environments (cbk).
+

September 2007. +The specification of Î»Î´ in +Matita 0.4 is online.
+

December 2005. First communication on Î»Î´.
+

May 2004. The specification of Î»Î´ in +Coq 7.3.1 begins.
+

Visibility

November 2010. The Google +search formal system lambda delta +gives 8 resources about Î»Î´ as the first results.
+

November 2010. The Yahoo +search formal system lambda delta +gives 4 resources and 2 sub-resources about Î»Î´ as the first results.

+
+

+
+Last update 2010-12-14 by Ferruccio +Guidi
+

The Formal System Î»Î´ (lambda-delta) +

Towards the unification of terms, types, environments and contexts

Documentation

Basic Î»Î´ version 2:

Basic Î»Î´ version 1:

The Formal System Î»Î´ (lambda-delta) +

Towards the unification of terms, types, environments and contexts

Computer-checked formal +specifications

Tools

Other resources

The Formal System Î»Î´ (lambda-delta) +

Towards the unification of terms, types, environments and contexts

Foreword

Notice +for +the +Internet +Explorer +user

The Formal System Î»Î´ (lambda-delta) +

Towards the unification of terms, types, environments and contexts

News

Visibility

The Formal System Î»Î´ (lambda-delta)
+

The Formal System Î»Î´ (lambda-delta)
+

The Formal System Î»Î´ (lambda-delta)
+

The Formal System Î»Î´ (lambda-delta)
+