Characterizing strong normalization in the Curien–Herbelin symmetric lambda calculus: Extending the Coppo–Dezani heritage

We develop an intersection type system for the  calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for : in addition to characterizing the  expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.