Document Type

Article

Date

1993

Embargo Period

12-19-2012

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.

Creative Commons License

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.