LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
3.30pm, Thursday 5th June 1997

*NOTE NONSTANDARD DAY AND TIME (Colloquium Slot)*

Title: Affine/Intuitionistic Typing for Idealized Algol

Speaker: Peter O'Hearn (Queen Mary and Westfield College, University of London)

Syntactic control of interference, or SCI, is a typing discipline described by John Reynolds in the late seventies. SCI is a restricted version of Idealized Algol, which is a simply-typed lambda-calculus with "imperative base types" such as a type of commands. In a basic version the restriction is simply to use an affine lambda calculus instead of the full (intuitionistic) typed calculus: the absence of Contraction has the effect of banishing aliasing and other forms of interference between different identifiers. In this talk I describe a language that allows the restrictions of SCI to be relaxed in local contexts. The language is based on a type system that mixes intuitionistic and affine function types, and has Idealized Algol and SCI as sublanguages. The type system uses a "bunch formalism" for typing contexts, following a method of mixing additive and multiplicative features used by Stephen Read in his formulations of relevant logics.