Relational semantics for effect-based program transformations with dynamic allocation

Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann

doi:10.1145/1273920.1273932

Relational semantics for effect-based program transformations with dynamic allocation

Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

27 Scopus citations

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.

Original language	English (US)
Title of host publication	PPDP'07
Subtitle of host publication	Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Pages	87-96
Number of pages	10
DOIs	https://doi.org/10.1145/1273920.1273932
State	Published - 2007
Externally published	Yes
Event	9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'07 - Wroclaw, Poland Duration: Jul 14 2007 → Jul 16 2007

Publication series

Name	PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

Conference

Conference	9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'07
Country/Territory	Poland
City	Wroclaw
Period	7/14/07 → 7/16/07

All Science Journal Classification (ASJC) codes

Software

Keywords

Logical relations
Parametricity
Program transformation
Region analysis
Type and effect systems

Access to Document

10.1145/1273920.1273932

Cite this

Benton, N., Kennedy, A., Beringer, L., & Hofmann, M. (2007). Relational semantics for effect-based program transformations with dynamic allocation. In PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (pp. 87-96). (PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming). https://doi.org/10.1145/1273920.1273932

Benton, Nick ; Kennedy, Andrew ; Beringer, Lennart et al. / Relational semantics for effect-based program transformations with dynamic allocation. PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2007. pp. 87-96 (PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming).

@inproceedings{321951166ceb43899b8fd7fa2d8885fa,

title = "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.",

keywords = "Logical relations, Parametricity, Program transformation, Region analysis, Type and effect systems",

author = "Nick Benton and Andrew Kennedy and Lennart Beringer and Martin Hofmann",

year = "2007",

doi = "10.1145/1273920.1273932",

language = "English (US)",

isbn = "1595937692",

series = "PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming",

pages = "87--96",

booktitle = "PPDP'07",

note = "9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'07 ; Conference date: 14-07-2007 Through 16-07-2007",

}

Benton, N, Kennedy, A, Beringer, L & Hofmann, M 2007, Relational semantics for effect-based program transformations with dynamic allocation. in PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 87-96, 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'07, Wroclaw, Poland, 7/14/07. https://doi.org/10.1145/1273920.1273932

Relational semantics for effect-based program transformations with dynamic allocation. / Benton, Nick; Kennedy, Andrew; Beringer, Lennart et al.
PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2007. p. 87-96 (PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Relational semantics for effect-based program transformations with dynamic allocation

AU - Benton, Nick

AU - Kennedy, Andrew

AU - Beringer, Lennart

AU - Hofmann, Martin

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - Logical relations

KW - Parametricity

KW - Program transformation

KW - Region analysis

KW - Type and effect systems

UR - http://www.scopus.com/inward/record.url?scp=34548099236&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34548099236&partnerID=8YFLogxK

U2 - 10.1145/1273920.1273932

DO - 10.1145/1273920.1273932

M3 - Conference contribution

AN - SCOPUS:34548099236

SN - 1595937692

SN - 9781595937698

T3 - PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

SP - 87

EP - 96

BT - PPDP'07

T2 - 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'07

Y2 - 14 July 2007 through 16 July 2007

ER -

Benton N, Kennedy A, Beringer L, Hofmann M. Relational semantics for effect-based program transformations with dynamic allocation. In PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2007. p. 87-96. (PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming). doi: 10.1145/1273920.1273932

Relational semantics for effect-based program transformations with dynamic allocation

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this