A Fibrational Account of Local States - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

A Fibrational Account of Local States

Résumé

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.
Fichier principal
Vignette du fichier
fibrational-view-of-local-states.pdf (311.12 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03066087 , version 1 (15-12-2020)

Identifiants

Citer

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⟩
44 Consultations
281 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More