Abstract
We present a local relational reasoning method for reasoning about contextual equivalence of expressions in a λ-calculus with recursive types and general references. Our development builds on the work of Benton and Leperchey, who devised a nominal semantics and a local relational reasoning method for a language with simple types and simple references. Their method uses a parameterized logical relation. Here we extend their approach to recursive types and general references. For the extension, we build upon Pitts’ and Shinwell’s work on relational reasoning about recursive types (but no references) in nominal semantics. The extension is non-trivial because of general references (higher-order store) and makes use of some new ideas for proving the existence of the parameterized logical relation and for the choice of parameters.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 69–83. Springer, Heidelberg (2006)
Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 86–101. Springer, Heidelberg (2005)
Birkedal, L., Harper, R.: Constructing interpretations of recursive types in an operational setting. Information and Computation 155, 3–63 (1999)
Koutavas, V., Wand, M.: Bisimulations for untyped imperative objects. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 146–161. Springer, Heidelberg (2006)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: POPL 2006: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 141–152. ACM Press, New York (2006)
Mason, I.A., Smith, S., Talcott, C.L.: From operational semantics to domain theory. Information and Computation 128(1), 26–47 (1996)
Pitts, A.: Relational properties of domains. Information and Computation 127, 66–90 (1996)
Pitts, A.M., Stark, I.: Observable properties of higher order functions that dynamically create local names, or: What’s new? In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 122–141. Springer, Heidelberg (1993)
Reddy, U., Yang, H.: Correctness of data representations involving heap data structures. Science of Computer Programming 50(1-3), 129–160 (2004)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, pp. 55–74. IEEE Press, Los Alamitos (2002)
Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, Computer Laboratory, Cambridge (December 2004)
Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science 342, 28–55 (2005)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. In: ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Long Beach, California (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bohr, N., Birkedal, L. (2006). Relational Reasoning for Recursive Types and References. In: Kobayashi, N. (eds) Programming Languages and Systems. APLAS 2006. Lecture Notes in Computer Science, vol 4279. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11924661_5
Download citation
DOI: https://doi.org/10.1007/11924661_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48937-5
Online ISBN: 978-3-540-48938-2
eBook Packages: Computer ScienceComputer Science (R0)