Algol-like Languages pp 297-329 | Cite as

# Linearity, Sharing and State: A Fully Abstract Game Semantics for Idealized Algol with Active Expressions

Chapter

## Abstract

The manipulation of objects with state which changes over time is all-pervasive in computing. Perhaps the simplest example of such objects are the program variables of classical imperative languages. An important strand of work within the study of such languages, pioneered by John Reynolds, focusses on Idealized Algol, an elegant synthesis of imperative and functional features.

## Keywords

Monoidal Category Linear Logic Program Variable Initial Move Legal Position
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- [1]S. Abramsky. Axioms for full abstraction and full completeness. Submitted for publication, 1996.Google Scholar
- [2]S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Submitted for publication, 1996.Google Scholar
- [3]S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors,
*Handbook of Logic in Computer Science*, Volume 3, pages 1168. Oxford University Press, 1994.Google Scholar - [4]A. Asperti and G. Longo.
*Categories*,*Types and Structures: An introduction to category theory for the working computer scientist*. The MIT Press, 1991.Google Scholar - [5]G. Berry, P.-L. Curien, and J.-J. Lévy. Full abstraction for sequential languages: the state of the art. In M. Nivat and J. C. Reynolds, editors,
*Algebraic Semantics*, pages 89–132. Cambridge University Press, 1986.Google Scholar - [6]G. Bierman. What is a categorical model of intuitionistic linear logic? In
*Proceedings of the Second International Conference on Typed A-calculi and Applications*, pages 78–93.*Lecture Notes in Computer Science*, volume 902, Springer-Verlag, 1995.Google Scholar - [7]F. Borceux.
*Handbook of Categorical Algebra*, volume 1. Cambridge University Press, 1994.Google Scholar - [8]R. Cartwright, P.-L. Curien, and M. Felleisen. Fully abstract semantics for observably sequential languages.
*Information and Computation*, 111 (1): 297–401, 1994.MathSciNetMATHCrossRefGoogle Scholar - [9]R. Croie.
*Categories for Types*. Cambridge University Press, 1994.Google Scholar - [10]M. P. Fiore, E. Moggi, and D. Sangiorgi. A fully abstract model for the rr-calculus. In
*11th Annual IFFE Symposium on Logic in Computer Science*, pages 43–54 IFFF Computer Society Press, 1996.Google Scholar - [11]M. Hyland and C.H. L. Ong. On full abstraction for PCF. Submitted for publication, 1996.Google Scholar
- [12]R. Loader. Finitary PCF is undecidable. Unpublished manuscript, available from http: //info. ox. ac.uk/—loader/, 1996.Google Scholar
- [13]G. McCusker.
*Games and Full Abstraction for a Functional Metalanguage with Recursive Types*. PhD thesis, Imperial College, University of London, to appear.Google Scholar - [14]G. McCusker. Games and full abstraction for FPC. In
*11th Annual IFFF Symposium on Logic in Computer Science*, pages 174–183. IFFF, Computer Society Press, 1996.Google Scholar - [15]R. Milner. Processes: a mathematical model of computing agents. In
*Logic Colloquium*‘73, pages 157–173. North Holland, 1975.Google Scholar - [16]R. Milner.
*A Calculus of Communicating Systems*. Springer-Verlag, 1980.Google Scholar - [17]R. Milner. Functions as processes.
*Mathematical Structures in Computer Science*, 2 (2): 119–142, 1992.MathSciNetMATHCrossRefGoogle Scholar - [18]P. W. O’Hearn and U. Reddy. Objects, interference and the Yoneda embedding. In M. Main and S. Brookes, editors,
*Mathematical Foundations of Programming Semantics: Proceedings of 11th International Conference*,*Electronic Notes in Theoretical Computer Science*, volume 1. Elsevier Science, 1995.Google Scholar - [19]P. W. O’Hearn, M. Takayama, A. J. Power, and R. D. Tennent. Syntactic control of interference revisited. In M. Main and S. Brookes, editors,
*Mathematical Foundations of Programming Semantics: Proceedings of 11th International Conference*,*Electronic Notes in Theoretical Computer Science*, volume 1. Elsevier Science, 1995. See Chapter 18.Google Scholar - [20]P. W. O’Hearn and R. D. Tennent. Parametricity and local variables.
*Journal of the ACM*,42(3):658–709, May 1995. See Chapter 16.Google Scholar - [21]F. J. Oles. Type categories, functor categories and block structure. In M. Nivat and J. C. Reynolds, editors,
*Algebraic Semantics*. Cambridge University Press, 1985. See Chapter 11.Google Scholar - [22]C.-H. L. Ong and C. A. Stewart. A Curry-Howard foundation for functional computation with control (summary). Preprint, July 1996.Google Scholar
- [23]A. M. Pitts. Reasoning about local variables with operationally-based logical relations. In
*11th Annual JEFF Symposium on Logic in Computer Science*,pages 152–163. IFFF Computer Society Press, 1996. See Chapter 17.Google Scholar - [24]G. Plotkin. LCF considered as a programming language.
*Theoretical Computer Science*, 5: 223–255, 1977.MathSciNetCrossRefGoogle Scholar - [25]U. Reddy. Global state considered unncessary: Introduction to object-based semantics.
*LISP and Functional Programming*,9(1):7–76, 1996. See Chapter 19.Google Scholar - [26]J. C. Reynolds. Syntactic control of interference. In
*Con f. Record 5th ACM Symposium on Principles of Programming Languages*,pages 39–46, 1978. See Chapter 10.Google Scholar - [27]J. C. Reynolds. The essence of ALGOL. In J. W. de Bakker and J. C. van Vliet, editors,
*Algorithmic Languages*, pages 345–372. North Holland, 1981. See Chapter 3.Google Scholar - [28]R. A. G. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In
*Category theory*,*Computer Science and Logic*. American Mathematical Society Contemporary Mathematics, volume 92, 1989.Google Scholar - [29]K. Sieber.
*Full Abstraction for the Second-Order Subset of an ALGOL-like Language*. Technischer Bericht A/04/95, FB14, Universität des Saarlandes, 1995. See Chapter 15.Google Scholar - [30]I. Stark.
*Names and Higher-Order Functions*. PhD thesis, University of Cambridge, December 1994.Google Scholar - [31]I. Stark. A fully abstract domain model for the rr-calculus. In
*11th Annual JEFF Symposium on Logic in Computer Science*. IFFF Computer Society Press, 1996.Google Scholar - [32]R. D. Tennent. Denotational semantics. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors,
*Handbook of Logic in Computer Science*, volume 3, pages 169322. Oxford University Press, 1994.Google Scholar - [33]G. Winskel.
*The Formal Semantics of Programming Languages*. The MIT Press, 1993.Google Scholar

## Copyright information

© Springer Science+Business Media New York 1997