A monad for full ground reference cells

Authors Ohad Kammar, Paul Blain Levy, Sean Moss, Sam Staton

Publication date 19 January 2021

Full work available at URL https://arxiv.org/abs/1702.04908, http://dl.acm.org/citation.cfm?id=3330044

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Functor categories, comma categories (18A25)

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.

Recommendations

Cited in

(6)

This page was built for publication: A monad for full ground reference cells

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5144656)