  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.
