A monad for full ground reference cells

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish
Title of host publication2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Place of PublicationReykjavik, Iceland
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages12
ISBN (Electronic)978-1-5090-3018-7
ISBN (Print)978-1-5090-3019-4
Publication statusPublished - 1 Jun 2017
Event2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017


Conference2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2017
Internet address


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

Fingerprint Dive into the research topics of 'A monad for full ground reference cells'. Together they form a unique fingerprint.

Cite this