Game semantics for interface middleweight Java

ABSTRACT

We consider an object calculus in which open terms interact with the environment through interfaces. The calculus is intended to capture the essence of contextual interactions of Middleweight Java code. Using game semantics, we provide fully abstract models for the induced notions of contextual approximation and equivalence. These are the first denotational models of this kind.

References

1. M. Abadi and L. Cardelli. A theory of objects. Springer Verlag, 1996.
2. E. Ábraham, M. M. Bonsangue, F. S. de Boer, A. Gruener, and M. Steffen. Observability, connectivity, and replay in a sequential calculus of classes. In Proceedings of FMCO, 2004.
3. S. Abramsky, D. R. Ghica, A. S. Murawski, C.-H. L. Ong, and I. D. B. Stark. Nominal games and full abstraction for the nu-calculus. In Proceedings of LICS, 2004.
4. S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163:409--470, 2000.
5. S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In Algol-like languages, pages 297--329. Birkhaüser, 1997.
6. S. Abramsky and G. McCusker. Game semantics. In Logic and Computation: Marktoberdorf Proceedings. Springer-Verlag, 1998.
7. J. Alves-Foss, editor. Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science. Springer, 1999.
8. J. Alves-Foss and F. S. Lam. Dynamic denotational semantics of Java. In Formal Syntax and Semantics of Java, pages 201--240. 1999.
9. G.M. Bierman, M.J. Parkinson, and A.M. Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical Report 563, Computer Laboratory, University of Cambridge, 2002.
10. H. Björklund and T. Schwentick. On notions of regularity for data languages. Theor. Comput. Sci., 411(4--5):702--715, 2010.
11. M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13:341--363, 2002.
12. J. M. E. Hyland and C.-H. L. Ong. On Full Abstraction for PCF. Information and Computation, 163(2):285--408, 2000.
13. A. Jeffrey and J. Rathke. Java Jr: Fully abstract trace semantics for a core Java language. In Proceedings of ESOP, 2003.
14. A. Jeffrey and J. Rathke. A fully abstract may testing semantics for concurrent objects. Theor. Comput. Sci., 338(1--3):17--63, 2005.
15. S. N. Kamin and U. S. Reddy. Two semantic models of object-oriented languages. In Theoretical Aspects of Object Oriented Programming, pages 463--495. MIT Press, 1994.
16. V. Koutavas and M. Wand. Reasoning about class behavior. In Proceedings of FOOL/WOOD, 2007.
17. J. Laird. A game semantics of local names and good variables. In Proceedings of FOSSACS, 2004.
18. J. Laird. Game semantics for higher-order concurrency. In Proceedings of FSTTCS, 2006.
19. J. Laird. Game semantics for call-by-value polymorphism. In Proceedings of ICALP, 2010.
20. S. B. Lassen and P. B. Levy. Typed normal form bisimulation for parametric polymorphism. In Proceedings of LICS, 2008.
21. R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4(1):1--22, 1977.
22. E. Moggi. Computational lambda-calculus and monads. In Proceedings of LICS, 1989.
23. A. S. Murawski and N. Tzevelekos. Algorithmic nominal game semantics. In Proceedings of ESOP, 2011.
24. A. S. Murawski and N. Tzevelekos. Game semantics for good general references. In Proceedings of LICS, 2011.
25. J. Power and E. Robinson. Premonoidal categories and notions of computation. Math. Struct. in Comput. Sci., 7:453--468, 1997.
26. N. Tzevelekos. Full abstraction for nominal general references. Logical Methods in Computer Science, 5(3), 2009.
27. N. Tzevelekos. Fresh-register automata. In Proc. of POPL, 2011.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

      • Semantics

• Theory of computation

  • Semantics and reasoning

    • Program semantics

      • Denotational semantics