Functor categories, comma categories (18A25) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)
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
(8)- Category-theoretic structure for independence and conditional independence
- Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
- Local local reasoning: a BI-hyperdoctrine for full ground store
- scientific article; zbMATH DE number 7449991 (Why is no real title available?)
- scientific article; zbMATH DE number 7779295 (Why is no real title available?)
- An algebraic theory for shared-state concurrency
- Towards univalent reference types: the impact of univalence on denotational semantics
- A practical formalization of monadic equational reasoning in dependent-type theory
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)
