2026-08-25T22:09:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27359 2026-08-24T14:08:31Z ddc:004 open_access

Coinductive Reasoning for Parametrized Functors and Monads Dal Lago, Ugo Galal, Zeinab categorical semantics parametrized monads effects relations lax extensions behavioral equivalence coalgebra global state Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ugo Dal Lago and Zeinab Galal 2026 Is Part Of LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2026.29 urn:nbn:de:0030-drops-273598 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.29 eng https://creativecommons.org/licenses/by/4.0/legalcode