# Affine/Intuitionistic Typing for Idealized Algol

Peter O'Hearn (Queen Mary and Westfield College, University of London) LFCS Theory Seminar Room 2511, JCMB, King's Buildings 3.30pm, Thursday 5th June 1997

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 (intuitionist) 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 intuitionist and affine function types, and has Idealized Algol and SCI as sub-languages. 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.