Document Type
Article
Date
1993
Keywords
programming languages, interference, storage variables
Language
English
Disciplines
Programming Languages and Compilers
Description/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 don’t write to any storage variables – is shown to be closely related, in this model, to Girard’s “of course” modality.
Recommended Citation
O'Hearn, P. W., "A Model for Syntactic Control of Interference" (1993). L.C. Smith College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects. Paper 7.
http://surface.syr.edu/lcsmith_other/7