Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-24T07:43:14.626Z Has data issue: false hasContentIssue false
  • English
  • Français

The impact of higher-order state and control effects on local relational reasoning

Part of: JFP Research Articles

Published online by Cambridge University Press:  15 August 2012

DEREK DREYER ,
GEORG NEIS  and
LARS BIRKEDAL
DEREK DREYER
Affiliation:
Max Planck Institute for Software Systems (MPI-SWS) (e-mail: dreyer@mpi-sws.org, neis@mpi-sws.org)
GEORG NEIS
Affiliation:
Max Planck Institute for Software Systems (MPI-SWS) (e-mail: dreyer@mpi-sws.org, neis@mpi-sws.org)
LARS BIRKEDAL
Affiliation:
IT University of Copenhagen (e-mail: birkedal@itu.dk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages—languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the “semantic cube”: fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences.

In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke logical relations. Building on recent work of Ahmed et al. (2009), we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power of our language—namely, the restriction to first-order state and/or the removal of call/cc—we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time.

Type
Articles
Information
Journal of Functional Programming , Volume 22 , Special Issue 4-5: ICFP 2010 , September 2012 , pp. 477 - 528
Copyright
Copyright © Cambridge University Press 2012

References

Abramsky, S., Honda, K. & McCusker, G. (1998) A fully abstract game semantics for general references. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).Google Scholar
Ahmed, A. (2004) Semantics of Types for Mutable State. PhD. thesis. Princeton University.Google Scholar
Ahmed, A., Dreyer, D. & Rossberg, A. (2009) State-dependent representation independence. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Appel, A. & McAllester, D. (2001) An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23 (5), 657–683.CrossRefGoogle Scholar
Benton, N. & Hur, C.-K. (2009) Biorthogonality, step-indexing and compiler correctness. Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP).CrossRefGoogle Scholar
Benton, N. & Tabareau, N. (2009) Compiling functional types to relational specifications for low level imperative code. Proceedings of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI).CrossRefGoogle Scholar
Birkedal, L., Møgelberg, R., Schwinghammer, J. & Støvring, K. (January 2011) First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).CrossRefGoogle Scholar
Bohr, N. (2007) Advances in Reasoning Principles for Contextual Equivalence and Termination. PhD. thesis. IT University of Copenhagen.Google Scholar
Dreyer, D., Ahmed, A. & Birkedal, L. (2011) Logical step-indexed logical relations. Logical Methods Comput. Sci. 7 (2:16), 1–37.Google Scholar
Dreyer, D., Neis, G. & Birkedal, L. (2012) The Impact of Higher-Order State and Control Effects on Local Relational Reasoning (Technical Appendix). Tech. Rep. MPI-SWS-2012-001. Max Planck Institute for Software Systems (MPI-SWS), Germany. Available at: http://www.mpi-sws.org/tr/2012-001.pdf.Google Scholar
Dreyer, D., Neis, G., Rossberg, A. & Birkedal, L. (2010) A relational modal logic for higher-order stateful ADTs. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Felleisen, M. & Hieb, R. (1992) The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103 (2), 235–271.CrossRefGoogle Scholar
Friedman, D. & Haynes, C. (1985) Constraining control. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Ghica, Dan R. & McCusker, G. (2000) Reasoning about Idealized Algol using regular languages. Proceedings of International Colloquium on Automata, Languages and Programming (ICALP).CrossRefGoogle Scholar
Hur, C.-K. & Dreyer, D. (2011) A Kripke logical relation between ML and assembly. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Hur, C.-K., Dreyer, D., Neis, G. & Vafeiadis, V. (2012) The marriage of bisimulations and Kripke logical relations. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Johann, P. (2003) Short cut fusion is correct. J. Funct. Program. 13 (4), 797–814.CrossRefGoogle Scholar
Johann, P., Simpson, A. & Voigtländer, J. (2010) A generic operational metatheory for algebraic effects. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).CrossRefGoogle Scholar
Johann, P. & Voigtländer, J. (2006) The impact of seq on free theorems-based program transformations. Fundam. Inform. 69 (1–2), 63–102.Google Scholar
Koutavas, V. & Lassen, S. (February 2008) Fun with Fully Abstract Operational Game Semantics for General References. Unpublished.Google Scholar
Koutavas, V. & Wand, M. (2006) Small bisimulations for reasoning about higher-order imperative programs. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Krivine, J.-L. (1994) Classical logic, storage operators and second-order lambda-calculus. Ann. Pure Appl. Logic 68, 53–78.CrossRefGoogle Scholar
Laird, J. (1997) Full abstraction for functional languages with control. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).Google Scholar
Laird, J. (2007) A fully abstract trace semantics for general references. Proceedings of International Colloquium on Automata, Languages and Programming (ICALP).Google Scholar
Lassen, S. B. & Levy, P. B. (2007) Typed normal form bisimulation. Proceedings of Conference on Computer Science Logic (CSL).Google Scholar
Lassen, S. B. & Levy, P. B. (2008) Typed normal form bisimulation for parametric polymorphism. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).CrossRefGoogle Scholar
Mason, I. & Talcott, C. (1991) Equivalence in functional languages with effects. J. Funct. Program. 1 (3), 287–327.CrossRefGoogle Scholar
Morris, J. H. Jr. (1968) Lambda-Calculus Models of Programming Languages. PhD. thesis. Massachusetts Institute of Technology.Google Scholar
Murawski, A. S. (2005) Functions with local state: Regularity and undecidability. Theor. Comput. Sci. 338 (1–3), 315–349.CrossRefGoogle Scholar
Murawski, A. S. & Tzevelekos, N. (2011) Game semantics for good general references. 26th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society, pp. 75–84.Google Scholar
Murawski, A. S. & Walukiewicz, I. (2008) Third-order Idealized Algol with iteration is decidable. Theor. Comput. Sci. 390 (2–3), 214–229.CrossRefGoogle Scholar
O'Hearn, P. & Reddy, U. (1995) Objects, interference, and the Yoneda embedding. Proceedings of Conference on the Mathematical Foundations of Programming Semantics (MFPS).Google Scholar
Pilkiewicz, A. & Pottier, F. (2011) The essence of monotonic state. Proceedings of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI).CrossRefGoogle Scholar
Pitts, A. M. (1996) Reasoning about local variables with operationally-based logical relations. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).CrossRefGoogle Scholar
Pitts, A. (2005) Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Pierce, B. C. (ed), Chap. 7. MIT Press.Google Scholar
Pitts, A. & Stark, I. (1998) Operational reasoning for functions with local state. Proceedings of International Workshop on Higher Order Operational Techniques in Semantics (HOOTS).Google Scholar
Pottier, F. (2008) Hiding local state in direct style: A higher-order anti-frame rule. Proceedings of IEEE Symposium on Logic in Computer Science (LICS).CrossRefGoogle Scholar
Pottier, F. (2009) Generalizing the Higher-Order Frame and Anti-Frame Rules. Unpublished.Google Scholar
Reddy, U. S. & Dunphy, B. P. (2011) An automata-theoretic model of objects. Proceedings of International Workshop on Foundations of Object-Oriented Languages (FOOL).Google Scholar
Sangiorgi, D., Kobayashi, N. & Sumii, E. (2011) Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33 (1:5), 1–69.CrossRefGoogle Scholar
Schwinghammer, J., Birkedal, L., Pottier, F., Reus, B., Støvring, K. & Yang, H. (2012) A step-indexed Kripke model of hidden state. In Mathematical Structures in Computer Science. To appear.CrossRefGoogle Scholar
Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F. & Reus, B. (2010) A semantic foundation for hidden state. Proceedings of Foundations of Software Science and Computation Structures (FOSSACS).CrossRefGoogle Scholar
Støvring, K. & Lassen, S. B. (2007) A complete, co-inductive syntactic theory of sequential control and state. Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Sumii, E. (2009) A complete characterization of observational equivalence in polymorphic λ-calculus with general references. Proceedings of Conference on Computer Science Logic (CSL).CrossRefGoogle Scholar
Sumii, E. & Pierce, B. (2007) A bisimulation for type abstraction and recursion. J. ACM 54 (5), 1–43.CrossRefGoogle Scholar
Thielecke, H. (2000) On exceptions versus continuations in the presence of state. Proceedings of European Symposium on Programming (ESOP).CrossRefGoogle Scholar
Yoshida, N., Honda, K. & Berger, M. (2008) Logical Reasoning For Higher-Order Functions With Local State. Logical Methods Comput. Sci. 4 (4:2), 1–68.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.