Authors: Dougherty, Daniel
Ghilezan, Silvia 
Lescanne, Pierre
Title: A general technique for analyzing termination in symmetric proof calculi
Conference: WST'07 - The 9th International Workshop on Termination, Paris, France, July 2007
Issue Date: 2007
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.

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.