Relational Reasoning in a Nominal Semantics for Storage

1. Benton, N., Kennedy, A.: Monads, effects and transformations. In: 3rd International Workshop on Higher Order Operational Techniques in Semantics (HOOTS). Electronic Notes in Theoretical Computer Science, vol. 26. Elsevier, Amsterdam (1999)

   Google Scholar 

2. Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. Technical report, Microsoft Research (February 2005)

   Google Scholar 

3. Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, p. 232. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

4. Meyer, A.R., Sieber, K.: Towards a fully abstract semantics for local variables: Preliminary report. In: Proceedings of the 15th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (January 1988)

   Google Scholar 

5. O’Hearn, P.W., Reynolds, J.C.: From Algol to polymorphic linear lambda-calculus. Journal of the ACM 47(1), 167–223 (2000)

   Article  MATH  MathSciNet  Google Scholar 

6. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 1. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

7. O’Hearn, P.W., Tennent, R.D.: Parametricity and local variables. Journal of the ACM 42(3), 658–709 (1995)

   Article  MATH  MathSciNet  Google Scholar 

8. O’Hearn, P.W., Tennent, R.D. (eds.): Progress in Theoretical Computer Science, Algol-like Languages. Birkhäuser, Basel (1997) (Two volumes)

   Google Scholar 

9. Oles, F.J.: A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University (1982)

   Google Scholar 

10. Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: [8], (1997)

    Google Scholar 

11. Pitts, A.M., Stark, I.D.B.: 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)

    Google Scholar 

12. Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics. Publications of the Newton Institute, pp. 227–273. Cambridge University Press, Cambridge (1998)

    Google Scholar 

13. Pitts, A.M.: Relational properties of domains. Information and Computation 127(2) (1996)

    Google Scholar 

14. Reddy, U.S., Yang, H.: Correctness of data representations involving heap data structures. Science of Computer Programming 50(1-3), 129–160 (2004)

    Article  MATH  MathSciNet  Google Scholar 

15. Reynolds, J.C.: The essence of Algol. In: Proceedings of the International Symposium on Algorithmic Languages (1981), Reprinted in [8]

    Google Scholar 

16. Shinwell, M.R.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, Computer Laboratory, University of Cambridge (December 2004)

    Google Scholar 

17. Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. In: Theoretical Computer Science (2005) (To appear)

    Google Scholar 

18. Sieber, K.: New steps towards full abstraction for local variables. In: Proceedings of the ACM SIGPLAN Workshop on State in Programming Languages (1993)

    Google Scholar 

19. Stark, I.D.B.: Names and Higher-Order Functions. PhD thesis, Computer Laboratory, University of Cambridge, Available as Technical Report 363 (December 1994)

    Google Scholar 

20. Sumii, E., Pierce, B.C.: Logical relations for encryption. Journal of Computer Security 11(4) (2003)

    Google Scholar 

21. Tennent, R.D., Ghica, D.R.: Abstract models of storage. Higher-Order and Symbolic Computation 13(1/2), 119–129 (2000)

    Article  MATH  Google Scholar 

Download references