A Metalanguage for Guarded Iteration
Sergey Goncharov, Christoph Rauch, Lutz Schr\"oder

TL;DR
This paper introduces a generic metalanguage for guarded iteration that unifies various notions of recursion in programming languages, supported by categorical semantics and operational validation.
Contribution
It combines guardedness with call-by-value to create a unifying language for guarded and unguarded iteration with effects, supported by categorical semantics.
Findings
Categorical semantics for the metalanguage are developed.
A concrete operational semantics is provided for a specific instance.
Soundness and adequacy of the semantics are established.
Abstract
Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
