Nick Benton
ABSTRACT
We 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 recursively-defined domain interpreting the untyped language, with effect information interpreted in terms of the preservation of certain sets of binary relations on the store.
The semantics validates a number of effect-dependent program equivalences and can thus serve as a foundation for effect-based compiler transformations.
The definition of the semantics requires the solution of a mixed-variance equation which is not accessible to the hitherto known methods. We illustrate the difficulties with a number of small example equations one of which is still not known to have a solution.
- Amal J. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Peter Sestoft, editor, ESOP, volume 3924 of LNCS, pages 69--83. Springer, 2006. Google Scholar
Digital Library
- Amal J. Ahmed, Andrew W. Appel, and Roberto Virga. A stratified semantics of general references. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Proceedings. IEEE Computer Society, 2002. Google ScholarDigital Library
- 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, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect-based program transformations with dynamic allocation. In Proc. PPDP 2007, ACM, 2007. Google ScholarDigital Library
- L. Birkedal, K. Stovring, and J. Thamsborg. Relational parametricity for references and recursive types. In Types in Language Design and Implementation (TLDI), 2009. Google ScholarDigital Library
- Nina Bohr and Lars Birkedal. Relational reasoning for recursive types and references. In Naoki Kobayashi, editor, Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Proceedings, volume 4279 of LNCS, pages 79--96. Springer, 2006. Google ScholarDigital Library
- Hongxu Cai, Zhong Shao, and Alexander Vaynberg. Certified self-modifying code. In PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, pages 66--77, New York, NY, USA, 2007. ACM. Google ScholarDigital Library
- Martin Hofmann. Correctness of effect--based program transformations. In Orna Grumberg and Tobias Nipkow, editors, Formal Logical Methods for System Security and Correctness, pages 149--173. IOS Press, 2008.Google Scholar
- Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, pages 141--152, 2006. Google ScholarDigital Library
- A.M. Pitts. Relational properties of domains. Information and Computation, 127(2), 1996.Google Scholar
- Bernhard Reus and Jan Schwinghammer. Denotational semantics for Abadi and Leino's logic of objects. In Shmuel Sagiv, editor, Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Proceedings, volume 3444 of LNCS, pages 263--278. Springer, 2005. Google ScholarDigital Library
- J.C. Reynolds. On the relation between direct and continuation semantics. In Proceedings of the 2nd Colloquium on Automata, Languages and Programming. Springer-Verlag, 1974. Google ScholarDigital Library
- Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), Proceedings, pages 293--302. IEEE Computer Society, 2007. 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
Index Terms
- Relational semantics for effect-based program transformations: higher-order store
Recommendations
Relational semantics for effect-based program transformations with dynamic allocation
PPDP '07: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programmingWe 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 ...
Theorems for free for free: parametricity, with and without types
The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a ...
Logical relations for a logical framework
Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an important ...
Comments