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 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 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 λ→.

λδ comes in several versions listed in the following table, which includes the major milestones:

Version	Name	Started	Released	Dismissed
2	basic_2	April 2011	planned in 2013	not planned yet
1	basic_1	May 2004	November 2006	May 2008

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 2012-12-02 by Ferruccio Guidi