A general technique for analyzing termination in symmetric proof calculi

Abstract

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 on 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.