Nick Benton
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.
- M. Abadi. TT-closed relations and admissibility. Mathematical Structures in Computer Science, 10(3), 2000. Google Scholar
Digital Library
- S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Directions in Functional Programming, chapter 4, pages 65--116. Addison-Wesley, 1988. Google ScholarDigital Library
- A. Banerjee, N. Heintze, and J. Riecke. Region analysis and the polymorphic lambda calculus. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS), 1999. Google ScholarDigital Library
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. In 31st ACM Symposium on Principles of Programming Languages (POPL), 2004. Revised version available from http://research.microsoft.com/~nick/publications.htm. Google ScholarDigital Library
- N. Benton and P. Buchlovsky. Semantics of an effect analysis for exceptions. In 3rd ACM-SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), 2007. Google ScholarDigital Library
- N. Benton, J. Hughes, and E. Moggi. Monads and effects. In Applied Semantics, Advanced Lectures, volume 2395 of LNCS. Springer-Verlag, 2002. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In Applied Semantics, International Summer School, Springer LNCS 2395, pages 42--122, 2000. Google ScholarDigital Library
- N. Bohr and L. Birkedal. Relational reasoning for recursive types and references. In APLAS, 2006. Google ScholarDigital Library
- M. Fluet and G. Morrisett. Monadic regions. Journal of Functional Programming, 2006. to appear. Google ScholarDigital Library
- D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In ACM Conference on LISP and Functional Programming, Cambridge, Massachusetts, August 1986. Google ScholarDigital Library
- J. Y. Halpern, A. R. Meyer, and B. A. Trakhtenbrot. The semantics of local storage, or what makes the free-list free? In Proceedings of the 11th ACM Symposium on Principles of Programming Languages (POPL), 1984. Google ScholarDigital Library
- S. Peyton Jones and J. Launchbury. State in Haskell. Lisp and Symbolic Computation, 8(4), 1995. Google ScholarDigital Library
- Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, pages 141--152, 2006. Google ScholarDigital Library
- J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In 15th ACM Symposium on Principles of Programming Languages (POPL), 1988. Google ScholarDigital Library
- A. R. Meyer and K. Sieber. 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 ScholarDigital Library
- R. Milner. Communication and Concurrency. Prentice-Hall International, 1989. Google ScholarDigital Library
- E. Moggi and A. Sabry. Monadic encapsulation of effects: A revised approach (extended version). Journal of Functional Programming, 11(6), 2001. Google ScholarDigital Library
- D. Naumann. Observational purity and encapsulation. Theoretical Computer Science, To appear. Google ScholarDigital Library
- P. W. O'Hearn and R. D. Tennent. Parametricity and local variables. Journal of the ACM, 42(3):658--709, May 1995. Google ScholarDigital Library
- A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics. CUP, 1998. Google ScholarDigital Library
- U. S. Reddy and H. Yang. Correctness of data representations involving heap data structures. Science of Computer Programming, 50(1-3):129--160, March 2004. Google ScholarDigital Library
- B. Reus and J. Schwinghammer. Denotational semantics for a program logic of objects. Mathematical Structures in Computer Science, 2006. in press. Google ScholarDigital Library
- E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM Press, 2005. Google ScholarDigital Library
- R. D. Tennent and D. R. Ghica. Abstract models of storage. Higher-Order and Symbolic Computation, 13(1/2):119--129, 2000. Google ScholarDigital Library
- M. Tofte and J. -P. Talpin. Region-based memory management. Information and Computation, 132(2):109--176, 1997. Google ScholarDigital Library
- P. Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. Comput. Logic, 4(1):1--32, 2003. Google ScholarDigital Library
Index Terms
- Relational semantics for effect-based program transformations with dynamic allocation
Recommendations
Abstract effects and proof-relevant logical relations
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesWe give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or ...
Relational semantics for effect-based program transformations: higher-order store
PPDP '09: Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programmingWe give a denotational semantics to a type and effect system tracking reading and writing to global variables holding values that may include higher-order effectful functions. Refined types are modelled as partial equivalence relations over a ...
Effect-dependent transformations for concurrent programs
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative ProgrammingWe describe a denotational semantics for an abstract effect system for a higher-order, shared-variable concurrent language. The semantics validates general effect-based program equivalences, including sufficient conditions for replacing sequential ...
Comments