{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:22:51Z","timestamp":1779315771657,"version":"3.51.4"},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5572,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1993,12]]},"abstract":"<jats:p>Two imperative programming language phrases <jats:italic>interfere<\/jats:italic> 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 \u03bb-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.<\/jats:p><jats:p>We describe a category that has (an abstraction of) interference information built into all objects and maps. This information is used to define a \u2018tensor\u2019 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 - <jats:italic>i.e<\/jats:italic>. types for phrases that do not write to any storage variables - is shown to be closely related, in this model, to Girard's \u2018of course\u2019 modality.<\/jats:p>","DOI":"10.1017\/s0960129500000311","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:01:36Z","timestamp":1236157296000},"page":"435-465","source":"Crossref","is-referenced-by-count":16,"title":["A model for syntactic control of interference"],"prefix":"10.1017","volume":"3","author":[{"given":"P. W.","family":"O'Hearn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000311_ref042","volume-title":"Programming Concepts and Methods","author":"Wadler","year":"1990"},{"key":"S0960129500000311_ref041","unstructured":"Tennent R. D. (1992) The essence of functional programming. Conference Record of the 19th ACM Symposium on Principles of Programming Languages."},{"key":"S0960129500000311_ref040","volume-title":"Semantics of Programming Languages","author":"Tennent","year":"1991"},{"key":"S0960129500000311_ref039","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90045-J"},{"key":"S0960129500000311_ref038","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17162-2_124"},{"key":"S0960129500000311_ref037","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90123-2"},{"key":"S0960129500000311_ref036","doi-asserted-by":"crossref","unstructured":"Swarup V. , Reddy U. S. and Ireland E. (1991) Assignments for applicative languages. Proc. Conference on Functional Programming Languages and Computer Architecture.","DOI":"10.1007\/3540543961_10"},{"key":"S0960129500000311_ref034","volume-title":"International Conference on Theoretical Aspects of Computer Software","author":"Reynolds","year":"1991"},{"key":"S0960129500000311_ref033","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035793"},{"key":"S0960129500000311_ref032","volume-title":"Proc. 2nd IEEE Symposium on Logic in Computer Science","author":"Reynolds","year":"1987"},{"key":"S0960129500000311_ref031","first-page":"345","volume-title":"Algorithmic Languages","author":"Reynolds","year":"1981"},{"key":"S0960129500000311_ref029","doi-asserted-by":"publisher","DOI":"10.1145\/390017.808307"},{"key":"S0960129500000311_ref027","first-page":"543","volume-title":"Algebraic Methods in Semantics","author":"Oles","year":"1985"},{"key":"S0960129500000311_ref025","doi-asserted-by":"crossref","unstructured":"O'Hearn P. W. and Tennent R. D. (1993) Semantical analysis of specification logic, part 2. To appear in Information and Computation.","DOI":"10.1006\/inco.1993.1060"},{"key":"S0960129500000311_ref024","volume-title":"London Math. Soc. Lecture Notes Series","author":"O'Hearn","year":"1992"},{"key":"S0960129500000311_ref023","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013458"},{"key":"S0960129500000311_ref014","volume-title":"The Turing Programming Language. Design and Definition","author":"Holt","year":"1987"},{"key":"S0960129500000311_ref015","volume-title":"occam 2 Reference Manual","year":"1988"},{"key":"S0960129500000311_ref011","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"S0960129500000311_ref001","doi-asserted-by":"crossref","unstructured":"Abramsky S. (1993) Computational interpretations of linear logic. To appear in Theoretical Computer Science.","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"S0960129500000311_ref002","unstructured":"ANSI (1978) American National Standards Institute, Fortran Standard, ANSI X3.9."},{"key":"S0960129500000311_ref008","doi-asserted-by":"crossref","unstructured":"Guzm\u00e0n J. and Hudak P. (1990) Single-threaded polymorphic lambda calculus. Proceedings of the 5th IEEE Symposium on Logic in Computer Science 333\u2013345.","DOI":"10.1109\/LICS.1990.113759"},{"key":"S0960129500000311_ref017","volume-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek","year":"1986"},{"key":"S0960129500000311_ref028","doi-asserted-by":"publisher","DOI":"10.1145\/7902.7904"},{"key":"S0960129500000311_ref018","unstructured":"Lent A. F. (1992) The category of functors from state shapes to bottomless CPOs is adequate for block structure, Master's thesis, MIT."},{"key":"S0960129500000311_ref026","volume-title":"A Category-Theoretic Approach to the Semantics of Programming Languages","author":"Oles","year":"1982"},{"key":"S0960129500000311_ref013","volume-title":"Proceedings of the Workshop on Implementation of Lazy Functional Languages","author":"Holmstrom","year":"1988"},{"key":"S0960129500000311_ref030","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. (1978) Syntactic control of interference. Conference Record of the 5th ACM Symposium on Principles of Programming Languages 39\u201346.","DOI":"10.1145\/512760.512766"},{"key":"S0960129500000311_ref035","doi-asserted-by":"crossref","unstructured":"Seeley R. A. G. (1989) Linear logic, *-autonomous categories and cofree coalgebras. Contemporary Mathematics 92: Categories in Computer Science and Logic 371\u2013382.","DOI":"10.1090\/conm\/092\/1003210"},{"key":"S0960129500000311_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"S0960129500000311_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"S0960129500000311_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129500000311_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"S0960129500000311_ref006","volume-title":"Structured Programming","author":"Dahl","year":"1972"},{"key":"S0960129500000311_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129500000311_ref009","doi-asserted-by":"crossref","unstructured":"Halpern J. Y. , Meyer A. R. and Trakhtenbrot B. A. (1983) The semantics of local storage, or what makes the free list free? Conference Record of the 11th ACM Symposium on Principles of Programming Languages 245\u2013257.","DOI":"10.1145\/800017.800536"},{"key":"S0960129500000311_ref012","volume-title":"Technical Report CS-74\u2013403","author":"Hoare","year":"1974"},{"key":"S0960129500000311_ref004","volume-title":"Operating Systems Principles","author":"Brinch Hansen","year":"1973"},{"key":"S0960129500000311_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90100-4"},{"key":"S0960129500000311_ref019","doi-asserted-by":"crossref","unstructured":"Lucaseen J. M. and Gifford D. K. (1988) Polymorphic effect systems. Conference Record of the 15th ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/73560.73564"},{"key":"S0960129500000311_ref022","unstructured":"Moggi E. (1989) An abstract view of programming languages. Course Notes."},{"key":"S0960129500000311_ref021","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73577"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T20:54:39Z","timestamp":1557953679000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000311\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,12]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1993,12]]}},"alternative-id":["S0960129500000311"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000311","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,12]]}}}