Relational semantics for effect-based program transformations with dynamic allocation

ABSTRACT

We give a denotational semantics to a region-based effect system tracking reading, writing and allocation in a higher-order language with dynamically allocated integer references.

Effects are interpreted in terms of the preservation of certain binary relations on the store, parameterized by region-indexed partial bijections on locations.

The semantics validates a number of effect-dependent program equivalences and can thus serve as a foundation for effect-based compiler transformations.

REFERENCES

• 1: Martín Abadi, ⊤⊤-closed relations and admissibility, Mathematical Structures in Computer Science, v.10 n.3, p.313-320, June 2000 [doi>10.1017/S0960129500003054]
• 2: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 3: Anindya Banerjee , Nevin Heintze , Jon G. Riecke, Region Analysis and the Polymorphic Lambda Calculus, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.88, July 02-05, 1999
• 4: Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
• 5: Nick Benton , Peter Buchlovsky, Semantics of an effect analysis for exceptions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190320]
• 6: Nick Benton , John Hughes , Eugenio Moggi, Monads and Effects, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, p.42-122, September 09-15, 2000
• 7: N. Benton and A. Kennedy. Monads, effects and transformations. In 3rd International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), volume 26 of ENTCS. Elsevier, 1999.
• 8: N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Reading, writing, and relations: Towards extensional semantics for effect analyses. In 4th Asian Symposium on Programming Languages and Systems (APLAS), LNCS, 2006.
• 9: N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In 7th International Conference on Typed Lambda Calculi and Applications (TLCA), volume 3461 of LNCS, 2005.
• 10: Nick Benton , John Hughes , Eugenio Moggi, Monads and Effects, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, p.42-122, September 09-15, 2000
• 11: N. Bohr and L. Birkedal. Relational reasoning for recursive types and references. In APLAS, 2006.
• 12: Matthew Fluet , Greg Morrisett, Monadic regions, Journal of Functional Programming, v.16 n.4-5, p.485-545, July 2006 [doi>10.1017/S095679680600596X]
• 13: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 14: Joseph Y. Halpern , Albert R. Meyer , B. A. Trakhtenbrot, The semantics of local storage, or what makes the free-list free?(Preliminary Report), Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.245-257, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800536]
• 15: John Launchbury , Simon L. Peyton Jones, State in Haskell, Lisp and Symbolic Computation, v.8 n.4, p.293-341, Dec. 1995 [doi>10.1007/BF01018827]
• 16: Vasileios Koutavas , Mitchell Wand, Small bisimulations for reasoning about higher-order imperative programs, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.141-152, January 11-13, 2006, Charleston, South Carolina, USA
• 17: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 18: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 19: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 20: E. Moggi , Amr Sabry, Monadic encapsulation of effects: a revised approach (extended version), Journal of Functional Programming, v.11 n.6, p.591-627, November 2001 [doi>10.1017/S0956796801004154]
• 21: David A. Naumann, Observational purity and encapsulation, Theoretical Computer Science, v.376 n.3, p.205-224, May, 2007 [doi>10.1016/j.tcs.2007.02.004]
• 22: P. W. O'Hearn , R. D. Tennent, Parametricity and local variables, Journal of the ACM (JACM), v.42 n.3, p.658-709, May 1995 [doi>10.1145/210346.210425]
• 23: A. M. Pitts , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 24: Uday S. Reddy , Hongseok Yang, Correctness of data representations involving heap data structures, Science of Computer Programming, v.50 n.1-3, p.129-160, March 2004 [doi>10.1016/j.scico.2004.01.007]
• 25: Bernhard Reus , Jan Schwinghammer, Denotational semantics for a program logic of objects, Mathematical Structures in Computer Science, v.16 n.2, p.313-358, April 2006 [doi>10.1017/S0960129506005214]
• 26: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.63-74, January 12-14, 2005, Long Beach, California, USA
• 27: Robert D. Tennent , Dan R. Ghica, Abstract Models of Storage, Higher-Order and Symbolic Computation, v.13 n.1-2, p.119-129, April 2000 [doi>10.1023/A:1010022312623]
• 28: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 29: Philip Wadler , Peter Thiemann, The marriage of effects and monads, ACM Transactions on Computational Logic (TOCL), v.4 n.1, p.1-32, January 2003 [doi>10.1145/601775.601776]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Dynamic storage management

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis; Denotational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
logical relations, parametricity, program transformation, region analysis, type and effect systems