Skip to main content
SpringerLink
Log in
Book cover

Algol-like Languages pp 109–163Cite as

Birkhäuser

Parametricity and Local Variables

  • Chapter

  • 127 Accesses

Part of the book series: Progress in Theoretical Computer Science ((PTCS))

Abstract

We propose that the phenomenon of local state may be understood in terms of Strachey’s concept of parametric (i.e., uniform) polymorphism. The intuitive basis for our proposal is the following analogy: a non-local procedure is independent of locally-declared variables in the same way that a parametrically polymorphic function is independent of types to which it is instantiated.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Abramsky, S. And Jensen, T. P. 1991. A relational approach to strictness analysis for higher-order polymorphic functions. In Conference Record of the Eighteenth Acm Symposium on Principles of Programming Languages, Orlando, Florida. Acm, New York, pages 49–54.

    Google Scholar 

  • Amadio, R. M. 1989. Recursion over realizability structures. Information and Computation, 91: 55–85.

    Article  MathSciNet  Google Scholar 

  • Barr, M. And Wells, C. 1990. Category Theory for Computing Science. Prentice-Hall International, London.

    MATH  Google Scholar 

  • Coox, W. 1991. Object-oriented programming versus abstract data types. In Foundations of Object-Oriented Languages, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, volume 489 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, pages 151–178.

    Google Scholar 

  • Fourman, M. P., Johnstone, P. T., And Pitts, A. M., editors, 1992. Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, England.

    Google Scholar 

  • Freyd, P. J., Mulry, P., Rosolini, G., And Scott, D. S. 1990. Extensional Pers. In [Lics, 1990 ], pages 346–354.

    Google Scholar 

  • Freyd, P. J., Robinson, E. P., And Rosolini, G. 1992a. Dinaturality for free. I n [Fourman et al., 1992], pages 107–118.

    Google Scholar 

  • Freyd, P. J., Robinson, E. P., And Rosolini, G. 1992b. Functorial parametricity. In [Lics, 1992 ], pages 444–452.

    Google Scholar 

  • Goerdt, A. 1985. A Hoare calculus for functions defined by recursion on higher types. In Logics of Programs 1985, R. Parikh, editor, volume 193 of Lecture Notes in Computer Science, Brooklyn, N.Y. Springer-Verlag, Berlin, pages 106–117.

    Google Scholar 

  • Gries, D., editor, 1978. Programming Methodology, A Collection of Articles by Ifip WG 2.3. Springer-Verlag, New York.

    Google Scholar 

  • HoAre, C. A. R. 1972. Proof of correctness of data representations. Acta Informatica, 1:271–281. Reprinted in [Gries, 1978], pages 269–281.

    Google Scholar 

  • Honsell, F., Mason, I. A., Smith, S., And Talcorr, C. 1995. A variable typed logic of effects. Information and Computation, 119 (1): 55–90.

    Article  MathSciNet  MATH  Google Scholar 

  • Hyland, J., Robinson, E. P., And Rosolini, G. 1989. Algebraic types in Per models. In Mathematical Foundations of Programming Semantics, Proceedings of the 5th International Conference, M. Main et al., editors, volume 442 of Lecture Notes in Computer Science, Tulane University, New Orleans. Springer-Verlag, Berlin, 1990, pages 333–350.

    Google Scholar 

  • Hyland, J. M. E. 1988. A small complete category. Annals of Pure and Applied Logic, 40: 135–165.

    Article  MathSciNet  MATH  Google Scholar 

  • Johnstone, P. T. 1989. Affine categories and naturally Mal’cev categories. Journal of Pure and Applied Algebra, 61: 251–256.

    Article  MathSciNet  MATH  Google Scholar 

  • Kelly, G. M. And Street, R. H. 1974. Review of the basic elements of 2-categories. In Category Seminar: Proceedings Sydney Category Theory Seminar, 1972/1973, G. M. Kelly, editor, volume 420 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, pages 75–103.

    Google Scholar 

  • Lambek, J. And Scott, P. J. 1986. Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge, England.

    Google Scholar 

  • Lawvere, F. W. 1989. Qualitative distinctions between some toposes of generalized graphs. In Categories in Computer Science and Logic, J. W. Gray and A. Scedrov, editors, volume 92 of Contemporary Mathematics. American Mathematical Society, pages 261–300.

    Google Scholar 

  • Lics 1990. Proceedings, Fifth Annual Ifff Symposium on Logic in Computer Science, Philadelphia, PA. Ieee Computer Society Press, Los Alamitos, California.

    Google Scholar 

  • Lics 1992. Proceedings, 7th Annual Jeff Symposium on Logic in Computer Science, Santa Cruz, California. Ifff Computer Society Press, Los Alamitos, California.

    Google Scholar 

  • Lics 1994. Proceedings, Ninth Annual Ifff Symposium on Logic in Computer Science, Paris, France. Ieee Computer Society Press, Los Alamitos, California.

    Google Scholar 

  • LoNgo, G. And MoGgi, E. 1991. Constructive natural deduction and its “w-set” interpretation. Mathematical Structures in Computer Science, 1 (2): 215–254.

    Article  MathSciNet  Google Scholar 

  • MA, Q. And Reynolds, J. C. 1991. Types, abstraction, and parametric polymorphism, part 2. In Mathematical Foundations of Programming Semantics, Proceedings of the 7th International Conference, S. Brookes et al., editors, volume 598 of Lecture Notes in Computer Science, Pittsburgh, PA. Springer-Verlag, Berlin, 1992, pages 1–40.

    Google Scholar 

  • Mac Lane, S. 1971. Categories for the Working Mathematician. Springer-Verlag, New York.

    Book  MATH  Google Scholar 

  • Mason, I. A. And Talgott, C. L. 1992. References, local variables, and operational reasoning. In [Lics, 1992 ], pages 186–197.

    Google Scholar 

  • Meyer, A. R. And Sieber, K. 1988. Towards fully abstract semantics for local variables: preliminary report. In Conference Record of the Fifteenth Annual Acm Symposium on Principles of Programming Languages,San Diego, California. Acm, New York, pages 191–203. See Chapter 7.

    Google Scholar 

  • Mitchell, J. And Scedrov, A. 1992. Notes on sconing and relators. In Computer Science Logic: 6th Workshop, Csl ‘92: Selected Papers, E. Boerger et al., editors, volume 702 of Lecture Notes in Computer Science, San Miniato, Italy. Springer-Verlag, Berlin, 1993, pages 352–378.

    Google Scholar 

  • Mitchell, J. C. 1986. Representation independence and data abstraction. In Conference Record 13th Annual Acm Symposium on Principles of Programming Languages, St. Petersburg, Florida. Acm, New York, pages 263–276.

    Google Scholar 

  • Mitchell, J. C. 1990. Type systems for programming languages. In Handbook of Theoretical Computer Science, J. van Leeuwen, editor, volume B. Elsevier, Amsterdam, and The Mit Press, Cambridge, Mass., pages 365–458.

    Google Scholar 

  • Moggi, E. 1988. The maximum consistent theory of the second-order ßr1 lambda calculus. Unpublished note.

    Google Scholar 

  • Naur, P., Backus, J. W. ET AL. 1963. Revised report on the algorithmic language Algol 6o. Comm. Acm,6(1):1–17. Also The Computer Journal 5:349–67, and Numerische Mathematik 4:420–52. See Chapter 1.

    Google Scholar 

  • O’Hearn, P. W. And Reddy, U. S. 1995. Objects, interference, and the Yoneda embedding. In Mathematical Foundations of Programming Semantics, Eleventh Annual Conference,S. Brookes, M. Main, A. Melton, and M. Mislove, editors, volume 1 of Electronic Notes in Theoretical Computer Science,Tulane University, New Orleans, Louisiana. Elsevier Science.

    Google Scholar 

  • O’Hearn, P. W. And Tennent, R. D. 1992. Semantics of local variables. I n [Fourman et al., 1992], pages 217–238.

    Google Scholar 

  • O’Hearn, P. W. And Tennent, R. D. 1993a. Relational parametricity and local variables. In Conference Record of the Twentieth Annual Acm Sigplan-Sigact Symposium on Principles of Programming Languages, Charleston, South Carolina. Acm, New York, pages 171–184.

    Google Scholar 

  • O’Hearn, P. W. And Tennent, R. D. 1993b. Semantical analysis of specification logic, 2. Information and Computation,107(1):25–57. See Chapter 14.

    Google Scholar 

  • Oles, F. J. 1982. A Category-Theoretic Approach to the Semantics of Programming Languages. Ph.D. thesis, Syracuse University, Syracuse, N.Y. See Chapter 11.

    Google Scholar 

  • Oles, F. J. 1985. Type algebras, functor categories and block structure. In Algebraic Methods in Semantics,M. Nivat and J. C. Reynolds, editors. Cambridge University Press, Cambridge, England, pages 543–573. See Chapter 11.

    Google Scholar 

  • Phoa, W. 1990. Effective domains and intrinsic structure. In [Lics, 1990], pages 366377.

    Google Scholar 

  • Phoa, W. 1991. Two results on set-theoretic polymorphism. In Category Theory and Computer Science, D. H. Pitt et al., editors, volume 530 of Lecture Notes in Computer Science, Paris, France. Springer-Verlag, Berlin, pages 219–235.

    Google Scholar 

  • Pitts, A. And Stark, I. 1993a. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science, A. M. Borzyszkowski and S. Sokolowski, editors, volume 711 of Lecture Notes in Computer Science, Gdansk, Poland. Springer-Verlag, Berlin, pages 122–140.

    Google Scholar 

  • Pitts, A. And Stark, I. 1993b. On the observable properties of higher order functions that dynamically create local names (preliminary report). In [Sipl, 1993 ], pages 31–45.

    Google Scholar 

  • Prrrs, A. M. 1993. Relational properties of recursively defined domains. In Proceedings, 8th Annual Ieee Symposium on Logic in Computer Science, Montreal, Canada. Ifff Computer Society Press, Los Alamitos, California, pages 86–97.

    Google Scholar 

  • Plotkin, G. And Abadi, M. 1993. A logic for parametric polymorphism. In Typed Lambda Calculi and Applications, M. Bezen and J. F. Groote, editors, volume 664 of Lecture Notes in Computer Science, Utrecht, The Netherlands. Springer-Verlag, Berlin, pages 361–375.

    Google Scholar 

  • Plotkin, G. D. 1980. Lambda-definability in the full type hierarchy. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, editors. Academic Press, pages 363–373.

    Google Scholar 

  • Reddy, U. S. 1993. Global state considered unnecessary: semantics of interference-free imperative programming. In [Sipl, 1993 ], pages 120–135.

    Google Scholar 

  • Reddy, U. S. 1994. Passivity and independence. In [Lics, 1994 ], pages 342–352.

    Google Scholar 

  • Reddy, U. S. 1996. Global state considered unnecessary: Introduction to object-based semantics. LisP and Symbolic Computation,9(1):7–76, 1996. See Chapter 19.

    Google Scholar 

  • Reynolds, J. C. 1974. Towards a theory of type structure. In Proc. Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, Berlin. Springer-Verlag, pages 408–425.

    Google Scholar 

  • Reynolds, J. C. 1975. User-defined types and procedural data structures as complementary approaches to data abstraction. In New Advances in Algorithmic Languages 1975, S. A. Schuman, editor, Rocquencourt, France. Inst. de Reserche d’Informatique et d’Automatique, pages 157–168. Reprinted in [Gries, 1978 ], pages 309–317.

    Google Scholar 

  • Reynolds, J. C. 1978. Syntactic control of interference. In Conference Record of the Fifth Annual Acm Symposium on Principles of Programming Languages,Tucson, Arizona. Acm, New York, pages 39–46. See Chapter 10.

    Google Scholar 

  • Reynolds, J. C. 198la. The Craft of Programming. Prentice-Hall International, London.

    Google Scholar 

  • Reynolds, J. C. 198 lb. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, editors, Amsterdam. North-Holland, Amsterdam, pages 345–372. See Chapter 3.

    Google Scholar 

  • Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83, R. E. A. Mason, editor. North-Holland, Amsterdam, Paris, France, pages 513–523.

    Google Scholar 

  • Reynolds, J. C. And Plotkin, G. D. 1993. On functors expressible in the polymorphic typed lambda calculus. Information and Computation, 105 (1): 1–29.

    Article  MATH  Google Scholar 

  • Robinson, E. P. 1989. How complete is Per? In Proceedings, Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California Ifff Computer Society Press, pages 106–111.

    Google Scholar 

  • Robinson, E. P. And RosoLini, G. 1994. Reflexive graphs and parametric polymorphism. In [Lics, 1994 ], pages 364–371.

    Google Scholar 

  • Schmidt, D. A. 1985. Detecting global variables in denotational specifications. Acm Trans. on Programming Languages and Systems, 7 (3): 299–310.

    Article  MATH  Google Scholar 

  • Sieber, K. 1992. Reasoning about sequential functions via logical relations. I n [Four-man et al., 1992], pages 258–269.

    Google Scholar 

  • Sieber, K. 1993. New steps towards full abstraction for local variables. In [Sipl, 1993 ], pages 88–100.

    Google Scholar 

  • Sieber, K. 1994. Full abstraction for the second order subset of an Algol-like language. In Mathematical Foundations of Computer Science,volume 841 of Lecture Notes in Computer Science,Ktisice, Slovakia. Springer-Verlag, Berlin, pages 608617. See Chapter 15.

    Google Scholar 

  • Sipl 1993. Acm Sigplan Workshop on State in Programming Languages,Copenhagen

    Google Scholar 

  • Denmark, June 12. Technical report RR-968, Department of Computer Science, Yale University.

    Google Scholar 

  • Strachey, C. 1967. Fundamental Concepts in Programming Languages. Unpublished lecture notes, International Summer School in Computer Programming, Copenhagen.

    Google Scholar 

  • Tennent, R. D. 1989. Elementary data structures in Algol-like languages. Science of Computer Programming, 13: 73–110.

    Article  MathSciNet  MATH  Google Scholar 

  • Tennent, R. D. 1990. Semantical analysis of specification logic. Information and Computation,85(2):135–162. See Chapter 13.

    Google Scholar 

  • Tennent, R. D. 1991. Semantics of Programming Languages. International Series in Computer Science. Prentice-Hall International.

    Google Scholar 

  • Wadler, P. 1989. Theorems for free! In Functional Programming Languages and Computer Architecture, 4th International Symposium, Imperial College, London. Acm, New York, pages 347–359.

    Google Scholar 

Download references

Authors
  1. Peter W. O’Hearn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert D. Tennent
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Computer Science, Queen Mary & Westfield College, E1 4NS, England

    Peter W. O’Hearn

  2. Dept. of Computing and Information Science, Queen’s University, K7L 3N6, Kingston, Ontario, Canada

    Robert D. Tennent

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer Science+Business Media New York

About this chapter

Cite this chapter

O’Hearn, P.W., Tennent, R.D. (1997). Parametricity and Local Variables. In: O’Hearn, P.W., Tennent, R.D. (eds) Algol-like Languages. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4757-3851-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-1-4757-3851-3_6

  • Publisher Name: Birkhäuser, Boston, MA

  • Print ISBN: 978-1-4757-3853-7

  • Online ISBN: 978-1-4757-3851-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation