A monad for full ground reference cells

Ohad Kammar; P. B. Levy; S. K. Moss; Sam Staton

doi:10.1109/LICS.2017.8005109

A monad for full ground reference cells

Ohad Kammar, P. B. Levy, S. K. Moss, Sam Staton

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

Abstract

We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

Original language	English
Title of host publication	2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Place of Publication	Reykjavik, Iceland
Publisher	Institute of Electrical and Electronics Engineers
Pages	1-12
Number of pages	12
ISBN (Electronic)	978-1-5090-3018-7
ISBN (Print)	978-1-5090-3019-4
DOIs	https://doi.org/10.1109/LICS.2017.8005109
Publication status	Published - 1 Jun 2017
Event	2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017 http://lics.siglog.org/lics17/

Conference

Conference	2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2017
Country/Territory	Iceland
City	Reykjavik
Period	20/06/17 → 23/06/17
Internet address	http://lics.siglog.org/lics17/

Keywords / Materials (for Non-textual outputs)

calculus
formal logic
full ground reference cells
functor category
state monad transformer
encapsulation monad
call-by-value calculus
Resource management
Erbium

Access to Document

10.1109/LICS.2017.8005109

https://ieeexplore.ieee.org/document/8005109/

Cite this

@inproceedings{1e20ccfba865406c8eaba343fcb28087,

title = "A monad for full ground reference cells",

abstract = "We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.",

keywords = "calculus, formal logic, full ground reference cells, functor category, state monad transformer, encapsulation monad, call-by-value calculus, Resource management, Erbium",

author = "Ohad Kammar and Levy, {P. B.} and Moss, {S. K.} and Sam Staton",

year = "2017",

month = jun,

day = "1",

doi = "10.1109/LICS.2017.8005109",

language = "English",

isbn = "978-1-5090-3019-4",

pages = "1--12",

booktitle = "2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 ; Conference date: 20-06-2017 Through 23-06-2017",

url = "http://lics.siglog.org/lics17/",

}

Kammar, O, Levy, PB, Moss, SK & Staton, S 2017, A monad for full ground reference cells. in 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Institute of Electrical and Electronics Engineers, Reykjavik, Iceland, pp. 1-12, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, 20/06/17. https://doi.org/10.1109/LICS.2017.8005109

TY - GEN

T1 - A monad for full ground reference cells

AU - Kammar, Ohad

AU - Levy, P. B.

AU - Moss, S. K.

AU - Staton, Sam

PY - 2017/6/1

Y1 - 2017/6/1

N2 - We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

AB - We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

KW - calculus

KW - formal logic

KW - full ground reference cells

KW - functor category

KW - state monad transformer

KW - encapsulation monad

KW - call-by-value calculus

KW - Resource management

KW - Erbium

UR - https://ora.ox.ac.uk/objects/uuid:1640d0fd-917d-44c6-bc72-35ffc3d22c4e

U2 - 10.1109/LICS.2017.8005109

DO - 10.1109/LICS.2017.8005109

M3 - Conference contribution

SN - 978-1-5090-3019-4

SP - 1

EP - 12

BT - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - Institute of Electrical and Electronics Engineers

CY - Reykjavik, Iceland

T2 - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 20 June 2017 through 23 June 2017

ER -

A monad for full ground reference cells

Abstract

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Other files and links

Fingerprint

Ohad Kammar

Cite this

A monad for full ground reference cells

Abstract

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Other files and links

Fingerprint

Profiles

Ohad Kammar

Cite this