A model for syntactic control of interference

Open Access
Publisher Website
Google Scholar
Abstract
Two imperative programming language phrases interfere when one writes to a storage variable that the other reads from or writes to. Reynolds has described an elegant linguistic approach to controlling interference in which a refinement of typed λ-calculus is used to limit sharing of storage variables; in particular, different identifiers are required never to interfere. This paper examines semantic foundations of the approach.We describe a category that has (an abstraction of) interference information built into all objects and maps. This information is used to define a ‘tensor’ product whose components are required never to interfere. Environments are defined using the tensor, and procedure types are obtained via a suitable adjunction. The category is a model of intuitionistic linear logic. Reynolds' concept of passive type - i.e. types for phrases that do not write to any storage variables - is shown to be closely related, in this model, to Girard's ‘of course’ modality.

This publication has 23 references indexed in Scilit: