Section: New Results

Union and Intersection constraints

Participants : Luigi Liquori, Claude Stolze.

In [21], we introduced an explicitly typed $\lambda$-calculus with strong pairs, projections and explicit type coercions. The calculus can be parameterized with different intersection type theories, producing a family of calculi with related intersection typed systems. We proved the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We stated the relationship between the intersection type assignment systems and the corresponding intersection typed systems by means of an essence function translating an explicitly typed Delta-term into a pure $\lambda$-term one. We finally translated a term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The resulting generic calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.