Relational semantics for effect-based program transformations

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Relational semantics for effect-based program transformations: higher-order store

Full text

Pdf (519 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Coimbra, Portugal

SESSION: Types table of contents

Pages 301-312

Year of Publication: 2009

ISBN:978-1-60558-568-0

Authors

Nick Benton	MS Research, Cambridge, United Kingdom
Andrew Kennedy	MSR Cambridge, Cambridge, United Kingdom
Lennart Beringer	LMU Munich, Munich, Germany
Martin Hofmann	LMU Munich, Munich, Germany

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 2, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599447 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	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.
	2	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.
	3	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.
	4	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.
	5	L. Birkedal, K. Stovring, and J. Thamsborg. Relational parametricity for references and recursive types. In Types in Language Design and Implementation (TLDI), 2009.
	6	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.
	7	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.
	8	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.
	9	Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, pages 141--152, 2006.
	10	A.M. Pitts. Relational properties of domains. Information and Computation, 127(2), 1996.
	11	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.
	12	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.
	13	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.
	14	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.