"new foundations must give new math"

from "The Basic Picture. Structures for constructive topology"

by Giovanni Sambin, Oxford University Press, forthcoming


To register send an e-mail to maietti @ math.unipd.it

Registration fee: 40 euros
(to be paid at arrival).

Under the patronage of

Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Italy

University of Padova, Italy

AILA (Italian Association of Logic and Applications), whose first president was Giovanni Sambin (from 1987 to 1994).

Abstracts » Guidi

Ferruccio Guidi

The Formal System lambda-delta

The formal system lambda-delta [1] is a typed lambda calculus that pursues unification of terms, types, environments and contexts while enjoying a well conceived meta-theory, which includes the commonly desired properties.

This system takes some features from the Automath-related calculi and some from the pure type systems, but it differs from both in that it does not include the \Pi construction while it provides for an abbreviation mechanism at the level of terms.

Because of these features, lambda-delta can serve as a formal specification language for the type theories that need a predicative foundation: for instance cTT (Martin-Lof) and mTT (Maietti-Sambin).

We will give an informal presentation of the calculus focusing on motivations, design features and main meta-theoretical properties.

[1] F. Guidi: The Formal System lambda-delta. To appear in ACM Transactions On Computational Logic. CoRR identifier cs/0611040.