Abstract:

We present the ∆-calculus, an explicitly typed λ-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories, as described in the Barendregt-Dekker-Statman book on λ-calculi with types, producing a family of ∆-calculi with related intersection typed systems. We show why annotating pure λ-calculus with intersection types is not easy: a classical example is the difficulty to decorate the bound variable of the explicitly typed polymorphic identity λx: ?.x such that the type of the identity is (σ → σ) ∩ (τ → τ ): previous attempts showed that the full power of the intersection type discipline can be easily lost. We show why intersection typed systems need a kind of synchronised reduction to fix the subject reduction theorem. The same problematics also appear when decorating λ-calculus with union-types. Finally, we show how the ∆-calculus can be raised to a ∆-framework by adding dependent-types as in the Edinburgh Logical Framework.