Sergey Goncharov - Representing Guardedness in Call-by-Value and Guarded Parametrized Monads

lmcs:13170 - Logical Methods in Computer Science, February 16, 2026, Volume 22, Issue 1 - https://doi.org/10.46298/lmcs-22(1:9)2026
Representing Guardedness in Call-by-Value and Guarded Parametrized MonadsArticle

Authors: Sergey Goncharov

Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration, respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parameterized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.


Volume: Volume 22, Issue 1
Secondary volumes: Selected Papers of the 8th International Conference on Formal Structures and Deduction (FSCD 2023)
Published on: February 16, 2026
Accepted on: November 26, 2025
Submitted on: March 4, 2024
Keywords: Logic in Computer Science

Consultation statistics

This page has been seen 384 times.
This article's PDF has been downloaded 205 times.