A monad for full ground reference cells

Ohad Kammar ( Department of Computer Science, University of Oxford )

10Mar
14:00 10th March 2017 ( week 8, Hilary Term 2017 )
Lecture Theatre B, Department of Computer Science

I will describe how to build a monad on a functor category to model

dynamic allocation of potentially cyclic memory cells. In particular

I'll explain how to tackle the challenge of "effect masking" which
means roughly that "if you don't need to know about memory access then

you can't detect it.", and use this monad to give a denotational
account of an ML-like language with reference cells, and validate
associated program transformations.

I will explain the main insight behind our construction: identifying
the collection of stores as an object in a different functor category

equipped with a monad for adding hiding/encapsulation capabilities to

the stores. I will then obtain the full ground storage monad by

applying a state monad transformer to the encapsulation monad.

The talk is based on work with: Paul B. Levy, Sean K. Moss, and Sam
Staton (http://arxiv.org/abs/1702.04908).