More Web Proxy on the site http://driver.im/

article

Program equivalence in a simple language with state

Author:

Nikos TzevelekosAuthors Info & Claims

Computer Languages, Systems and Structures, Volume 38, Issue 2

Pages 181 - 198

https://doi.org/10.1016/j.cl.2012.02.002

Published: 01 July 2012 Publication History

Abstract

We examine different approaches to reasoning about program equivalence in a higher-order language which incorporates a basic notion of state: references of unit type (names). In particular, we present three such methods stemming from logical relations, bisimulation techniques and game semantics respectively. The methods are tested against a surprisingly difficult example equivalence at second order which exploits the intricacies of the language with respect to privacy and flow of names, and the ensuing notion of local state.

References

[1]

Abramsky S. The lazy lambda calculus. In: Research topics in functional programming. Addison-Wesley; 1990. p. 65-116.

Digital Library

[2]

Abramsky S, Ghica DR, Murawski AS, Ong C-HL, Stark IDB. Nominal games and full abstraction for the nu-calculus. In: LICS; 2004. p. 150-9.

Digital Library

[3]

Abramsky, S., Jagadeesan, R. and Malacaria, P., Full abstraction for PCF. Information and Computation. v163 i2. 409-470.

Digital Library

[4]

Abramsky, S. and McCusker, G., Linearity, sharing and state: a fully abstract game semantics for Idealized Algol. In: O'Hearn, P., Tennent, R.D. (Eds.), Algol-like languages, vol. 2. Birkhäuser, Boston. pp. 297-329.

[5]

Abramsky S, Ong C-HL. Algorithmic game semantics and its applications, Final Report; 2006.

[6]

Abramsky S, Tzevelekos N. Introduction to categories and categorical logic. In: New Structures for Physics, Lecture notes in physics, vol. 813. Springer; 2011. p. 3-94 (available on the arXiv).

[7]

Ahmed A, Dreyer D, Rossberg A. State-dependent representation independence. In: POPL; 2009. p. 340-353.

Digital Library

[8]

Benton N, Koutavas V. A mechanized bisimulation for the nu-calculus, 2009. Symposium in Honor of Mitchell Wand; August 2009. Submitted to Higher Order and Symbolic Computation.

[9]

Bernstein KL, Stark EW. Operational semantics of a focusing debugger. In: MFPS, Electronic notes in theoretical computer science, vol. 1; 1995. p. 13-31.

[10]

Birkedal, L., Støvring, K. and Thamsborg, J., Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science. v20 i4. 655-703.

Digital Library

[11]

Dreyer D, Neis G, Birkedal L. The impact of higher-order state and control effects on local relational reasoning. In: ICFP; 2010. p. 143-56.

Digital Library

[12]

Gabbay, M. and Pitts, A.M., A new approach to abstract syntax with variable binding. Formal Aspects of Computing. v13 i3-5. 341-363.

[13]

Ghica DR. Applications of game semantics: from program analysis to hardware synthesis. In: LICS; 2009. p. 17-26.

Digital Library

[14]

Ghica DR, McCusker G. Reasoning about idealized algol using regular languages. In: ICALP, Lecture notes in computer science, vol. 1853; 2000. p. 103-15.

Digital Library

[15]

Gordon AD. Bisimilarity as a theory of functional programming. In: MFPS, Electronic notes in theoretical computer science, vol. 1; 1995. p. 232-52.

[16]

Gordon AD, Rees GD. Bisimilarity for a first-order calculus of objects with subtyping. In: POPL; 1996. p. 386-95.

Digital Library

[17]

Goubault-Larrecq, J., Lasota, S. and Nowak, D., Logical relations for monadic types. Mathematical Structures in Computer Science. v18 i6. 1169-1217.

Digital Library

[18]

Hennessy M, Milner R. On observing nondeterminism and concurrency. In: ICALP, Lecture notes in computer science, vol. 85; 1980. p. 299-309.

Digital Library

[19]

Honda, K. and Yoshida, N., Game-theoretic analysis of call-by-value computation. Theoretica Computer Science. v221 i1-2. 393-456.

Digital Library

[20]

Hopkins D, Murawski AS, Ong C-HL. A fragment of ML decidable by visibly pushdown automata. In: ICALP, Lecture notes in computer science, vol. 6756; 2011. p. 149-61.

Digital Library

[21]

Hyland, J.M.E. and Ong, C.-H.L., On full abstraction for PCF: I, II, and III. Information and Computation. v163 i2. 285-408.

Digital Library

[22]

Jeffrey A, Rathke J. Towards a theory of bisimulation for local names. In: LICS; 1999. p. 56-66.

Digital Library

[23]

Jeffrey, A. and Rathke, J., A theory of bisimulation for a fragment of concurrent ML with local names. Theoretical Computer Science. v323 i1-3. 1-48.

Digital Library

[24]

Koutavas V. Reasoning about imperative and higher-order programs. PhD thesis, Northeastern University; 2008.

Digital Library

[25]

Koutavas V, Levy PB, Sumii E. From applicative to environmental bisimulation. In: MFPS, Electronic notes in theoretical computer science, vol. 276; 2011. p. 215-35.

Digital Library

[26]

Koutavas V, Wand M. Bisimulations for untyped imperative objects. In: ESOP, Lecture notes in computer science, vol. 3924; 2006. p. 146-61.

Digital Library

[27]

Koutavas V, Wand M. Small bisimulations for reasoning about higher-order imperative programs. In POPL; 2006. p. 141-52.

Digital Library

[28]

Laird J. A game semantics of local names and good variables. In: FoSSaCS, Lecture notes in computer science, vol. 2987; 2004. p. 289-303.

[29]

Laird J. Game semantics for higher-order concurrency. In: FSTTCS, Lecture notes in computer science, vol. 4337; 2006. p. 417-28.

Digital Library

[30]

Laird, J., A game semantics of names and pointers. Annals of Pure and Applied Logic. v151 i2-3. 151-169.

[31]

Loader, R., Finitary PCF is not decidable. Theoretical Computer Science. v266. 342-364.

Digital Library

[32]

Moggi, E., Notions of computation and monads. Information and Computation. v93. 55-92.

Digital Library

[33]

Murawski AS, Tzevelekos N. Full abstraction for Reduced ML. In: FOSSACS, Lecture notes in computer science, vol. 5504; 2009. p. 32-47.

Digital Library

[34]

Murawski AS, Tzevelekos N. Algorithmic nominal game semantics. In: ESOP, Lecture notes in computer science, vol. 6602; 2011. p. 419-38.

Digital Library

[35]

Murawski AS, Tzevelekos N. Game semantics for good general references. In: LICS; 2011. p. 75-84.

Digital Library

[36]

Neven, F., Schwentick, T. and Vianu, V., Finite state machines for strings over infinite alphabets. ACM Transactions on Computational Logic. v5 i3. 403-435.

Digital Library

[37]

Nickau H. Hereditarily sequential functionals: a game-theoretic approach to sequentiality. PhD thesis, University of Siegen; 1996.

[38]

O'Hearn, P.W. and Riecke, J.G., Kripke logical relations and PCF. Information and Computation. v120 i1. 107-116.

Digital Library

[39]

Pitts AM, Stark IDB. Observable properties of higher order functions that dynamically create local names, or what's new? In: MFCS; 1993. p. 122-41.

Digital Library

[40]

Pitts, A.M. and Stark, I.D.B., Operational reasoning for functions with local state. 1998. Cambridge University Press.

[41]

Plotkin GD. λ-definability and logical relations. Technical Report SAI-RM-4, School of Artificial Intelligence, University of Edinburgh; 1973.

[42]

Sangiorgi, D., Kobayashi, N. and Sumii, E., Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems. v33 i1. 5

Digital Library

[43]

Sangiorgi, D. and Walker, D., The π-calculus: a theory of mobile processes. 2001. Cambridge University Press.

Digital Library

[44]

Sieber, K., Reasoning about sequential functions via logical relations. In: Fourman, M.P., Johnstone, P.T., Pitts, A.M. (Eds.), Applications of Categories in Computer Science, Cambridge University Press.

[45]

Stark IDB. Names and higher-order functions. PhD thesis, University of Cambridge; 1994.

[46]

Sumii E, Pierce BC. A bisimulation for dynamic sealing. In: POPL; 2004. p. 161-72.

Digital Library

[47]

Sumii, E. and Pierce, B.C., A bisimulation for type abstraction and recursion. Journal of the ACM. v54 i5.

Digital Library

[48]

Tait, W.W., Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic. v32 i2. 198-212.

[49]

Tiuryn J, Wand M. Untyped lambda-calculus with input-output. In: CAAP, Lecture notes in computer science, vol. 1059; 1996. p. 317-29.

Digital Library

[50]

Tzevelekos, N., Full abstraction for nominal general references. Logical Methods in Computer Science. v5 i3.

[51]

Tzevelekos N. Fresh-register automata, In: POPL; 2011. p. 295-306.

Digital Library

[52]

Zhang Y, Nowak D. Logical relations for dynamic name creation. In: CSL, Lecture notes in computer science, vol. 2803; 2003. p. 575-88.

Cited By

Wood TDrossopolou SLahiri SEisenbach S(2017)Modular Verification of Procedure Equivalence in the Presence of Memory AllocationProgramming Languages and Systems10.1007/978-3-662-54434-1_35(937-963)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_35
Lösch SPitts A(2014)Denotational Semantics with Nominal Scott DomainsJournal of the ACM10.1145/262952961:4(1-46)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2629529
Lösch SPitts A(2013)Full abstraction for nominal Scott domainsACM SIGPLAN Notices10.1145/2480359.242907348:1(3-14)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429073
Show More Cited By

Program equivalence in a simple language with state
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Program equivalence by circular reasoning
Abstract
We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation ...
A language-independent proof system for full program equivalence
Abstract
Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in ...
An equivalence-preserving CPS translation via multi-language semantics
ICFP '11

Language-based security relies on the assumption that all potential attacks follow the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Computer Languages, Systems and Structures

Computer Languages, Systems and Structures Volume 38, Issue 2

July, 2012

76 pages

ISSN:1477-8424

Issue’s Table of Contents

Copyright © Elsevier Ltd © 2012.

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 July 2012

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wood TDrossopolou SLahiri SEisenbach S(2017)Modular Verification of Procedure Equivalence in the Presence of Memory AllocationProgramming Languages and Systems10.1007/978-3-662-54434-1_35(937-963)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_35
Lösch SPitts A(2014)Denotational Semantics with Nominal Scott DomainsJournal of the ACM10.1145/262952961:4(1-46)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2629529
Lösch SPitts A(2013)Full abstraction for nominal Scott domainsACM SIGPLAN Notices10.1145/2480359.242907348:1(3-14)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429073
Lösch SPitts AGiacobazzi RCousot R(2013)Full abstraction for nominal Scott domainsProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429073(3-14)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429073

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents