Representing Guardedness in Call-By-Value

Goncharov S (2023)


Publication Type: Conference contribution

Publication year: 2023

Journal

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 260

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Rome IT

ISBN: 9783959772778

DOI: 10.4230/LIPIcs.FSCD.2023.34

Abstract

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 parametrized 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.

Authors with CRIS profile

How to cite

APA:

Goncharov, S. (2023). Representing Guardedness in Call-By-Value. In Marco Gaboardi, Femke van Raamsdonk (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Rome, IT: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Goncharov, Sergey. "Representing Guardedness in Call-By-Value." Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, Rome Ed. Marco Gaboardi, Femke van Raamsdonk, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2023.

BibTeX: Download