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

Abstract

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