The Delta-calculus: syntax and types

TL;DR

The paper introduces the Delta-calculus, a typed lambda-calculus framework with strong pairs, projections, and explicit coercions, supporting various intersection type theories and proven to have key properties like normalization and decidability.

Contribution

It defines a parametrized family of Delta-calculi with formal properties and relationships to existing intersection type systems, including translation and coherence results.

Findings

Proves Church-Rosser and strong normalization for the calculus.

Establishes decidability of type checking and reconstruction.

Provides translation between typed and pure lambda-terms.

Abstract

We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Salle', the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection type systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems a` la Curry and the corresponding intersection type systems a` la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.