2026-07-23T01:12:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23300 2025-06-25T13:20:36Z ddc:004 open_access

Monadic Type-And-Effect Soundness Dagnino, Francesco Giannini, Paola Zucca, Elena Effects monads type soundness We introduce the abstract notions of monadic operational semantics, a small-step semantics where computational effects are modularly modeled by a monad, and type-and-effect system, including effect types whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usual in the non-monadic case, we can express progress and subject reduction, and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects, equipped with an expressive type-and-effect system We provide proofs of progress and subject reduction, parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Francesco Dagnino and Paola Giannini and Elena Zucca 2025 Is Part Of LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2025.7 urn:nbn:de:0030-drops-233009 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.7 eng https://creativecommons.org/licenses/by/4.0/legalcode