"** new foundations must give new math**"

from

by Giovanni Sambin, Oxford University Press, forthcoming

Registration

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**

Bologna

**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.