Skip to Main content Skip to Navigation
Conference papers

A Fibrational Account of Local States

Abstract : One main challenge of the theory of computational effects is to understand how to combine various notions of effects in a meaningful way. Here, we study the particular case of the local state monad, which we would like to express as the result of combining together a family of global state monads parametrized by the number of available registers. To that purpose, we develop a notion of indexed monad inspired by the early work by Street, which refines and generalizes Power's recent notion of indexed Lawvere theory. One main achievement of the paper is to integrate the block structure necessary to encode allocation as part of the resulting notion of indexed state monad. We then explain how to recover the local state monad from the functorial data provided by our notion of indexed state monad. This reconstruction is based on the guiding idea that an algebra of the indexed state monad should be defined as a section of a 2-categorical notion of fibration associated to the indexed state monad by a Grothendieck construction.
Document type :
Conference papers
Complete list of metadata
Contributor : Kenji Maillard Connect in order to contact the contributor
Submitted on : Tuesday, December 15, 2020 - 10:00:04 AM
Last modification on : Monday, January 10, 2022 - 5:30:04 PM
Long-term archiving on: : Tuesday, March 16, 2021 - 6:47:47 PM


Files produced by the author(s)




Kenji Maillard, Paul-André Melliès. A Fibrational Account of Local States. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, France. pp.402-413, ⟨10.1109/LICS.2015.45⟩. ⟨hal-03066087⟩



Les métriques sont temporairement indisponibles