programming languages, interference, storage variables
Programming Languages and Compilers
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.
O'Hearn, Peter W., "A Model for Syntactic Control of Interference" (1993). College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects. 7.
Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.