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

摘要

We develop an intersection type system for the (λ{top}-)μ(μ{top}~) 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 (λ{top}-)μ(μ{top}~): in addition to characterizing the (λ{top}-)μ(μ{top}~) expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.