Characterizing strong normalization in the Curien Herbelin


Silvia Ghilezan, University of Novi Sad. 29 mars 2007 10:00 limd 2:00:00
Abstract:

In this talk, I will present an intersection type system for Curien Herbelin symmetric lambda calculus, that has been developed in the joint work with Dan Dougherty and Pierre Lescanne. The system completely characterizes strong normalization of the free (unrestricted) reduction. The proof uses a technique based on fixed points. The system enjoys subject reduction and subject expansion.