Document Open Access Logo

Polymorphic Game Semantics for Dynamic Binding

Author James Laird

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2016.27.pdf
  • Filesize: 0.59 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • Game semantics
  • denotational models
  • PCF
  • Idealized Algol

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present a game semantics for an expressive typing system for block-structured programs with late binding of variables and System F style polymorphism. As well as generic programs and abstract datatypes, this combination may be used to represent behaviour such as dynamic dispatch and method overriding.

We give a denotational models for a hierarchy of programming languages based on our typing system, including variants of PCF and Idealized Algol. These are obtained by extending  polymorphic game semantics to block-structured programs. We show that the categorical structure of our models can be used to give a new interpretation of dynamic binding, and establish definability properties by imposing constraints which are identical or similar to those used to characterize definability in PCF (innocence, well-bracketing, determinacy). Moreover, relaxing these  can similarly allow the interpretation of side-effects (state, control, non-determinism) - we show that in particular we may obtain a fully abstract semantics of polymorphic Idealized Algol with dynamic binding by following exactly the methodology employed in the simply-typed case.

Cite As Get BibTex

James Laird. Polymorphic Game Semantics for Dynamic Binding. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.27

Author Details

James Laird

References

  1. S. Abramsky. Axioms for full abstraction and full completeness. In Essays in Honour of Robin Milner. MIT Press, 1997. Google Scholar
  2. S. Abramsky and R. Jagadeesan. A game semantics for generic polymorphism. Annals of Pure and Applied Logic, 133(1):3-37, 2004. Google Scholar
  3. S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163:409-470, 2000. Google Scholar
  4. S. Abramsky and G. McCusker. Linearity, Sharing and State: a fully abstract game semantics for Idealized Algol with active expressions. In P.W. O'Hearn and R. Tennent, editors, Algol-like languages. Birkhauser, 1997. Google Scholar
  5. S. Abramsky, K. Honda and G. McCusker. A fully abstract games semantics for general references. In Proceedings of LICS'98. IEEE Press, 1998. URL: http://dx.doi.org/10.1109/LICS.1998.705669.
  6. D. Ghica, A. S. Murawaki, and C.-H. L. Ong. Syntactic control of concurrency. In Proceedings of ICALP'04, number 3142 in LNCS. Springer, 2004. Google Scholar
  7. J.-Y. Girard. Interprétation functionelle et elimination des coupures de l'arithmètique d'ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  8. R. Harmer. Games and Full Abstraction for Nondeterministic Languages. PhD thesis, Imperial College London, 1999. Google Scholar
  9. R. Harmer and G. McCusker. A fully abstract games semantics for finite non-determinism. In Proceedings of the Fourteenth Annual Symposium on Logic in Computer Science, LICS'99. IEEE Computer Society Press, 1998. Google Scholar
  10. D. Hughes. Games and definability for System F. In Proceedings of the Twelfth International syposium on Logic in Computer Science, LICS'97. IEEE Computer Society Press, 1997. Google Scholar
  11. J. M. E. Hyland. Game semantics. In Semantics and Logics of Computation (Publications of the Newton Institute). Cambridge University Press, 1995. Google Scholar
  12. J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Information and Computation, 163:285-408, 2000. Google Scholar
  13. Y. Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988. Google Scholar
  14. J. Laird. Full abstraction for functional languages with control. In Proceedings of LICS'97. IEEE Computer Society Press, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614931.
  15. J. Laird. A categorical semantics of higher-order store. In Proceedings of CTCS'02, number 69 in ENTCS. Elsevier, 2002. Google Scholar
  16. J. Laird. Game semantics for a polymorphic programming language. In Proceedings of LICS'10. IEEE Press, 2010. Google Scholar
  17. J. Laird. Game semantics for a polymorphic programming language. Journal of the ACM, 60(4), 2013. Google Scholar
  18. G. McCusker. Games and full abstraction for a functional metalanguage with recursive types. PhD thesis, Imperial College London, 1996. Cambridge University Press. Google Scholar
  19. G. McCusker. On the semantics of the bad-variable constructor in Algol-like languages. In Proceedings of MFPS XIX, ENTCS, 2003. To appear. Google Scholar
  20. J. Mitchell and G. Plotkin. Abstract types have existential type. ACM transactions on Programming Languages and Systems, 10(3):470-502, 1988. Google Scholar
  21. A. Pitts. Polymorphism is set-theoretic constructively. In D. Pitt, editor, Proceedings of CTCS'88, number 283 in LNCS. Springer, 1988. Google Scholar
  22. U. Reddy. Objects and classes in Algol-like languages. Information and Computation, 172(1):63-97, 2002. Google Scholar
  23. J. C. Reynolds. Towards a theory of type structure. In Proceedings of the Programming Symposium, Paris 1974, number 19 in LNCS. Springer, 1974. Google Scholar
  24. J. C. Reynolds. The essence of Algol. In Algorithmic Languages, pages 345-372. North Holland, 1981. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact