Ugo de'Liguoro (Università di Torino), Intersection types for lambda-calculi with control



We investigate lambda-calculi extended with control operators from the point of view of intersection type theories. Intersection types are a natural bridge between syntax and semantics and have been extensively used to characterize computational properties of the untyped lambda-calculus. We aim at extending these techniques and results to calculi with control, whose semantics is usually given either in terms of CPS translations or of abstract machines. Building over a denotational model of continuations due Streicher and Reus, that is a model of several such calculi (including Felleisen's lambda-C, Parigot's lambda-mu, De Groote and Saurin's Lambda-mu and Krivine's lambda/cc), and using Abramsky's ideas on domain logic, we show how type theories and type assignment systems can be obtained out of Streicher and Reus models as well as of the"extensional" variant by Nakazawa and Katsumata, all inducing filter models in the sense of Barendregt-Coppo-Dezani. We eventually mention some results about strongly normalizing terms of Parigot's lambda-mu and the approximation theorem for De Groote-Saurin's Lambda-mu.