A Metalanguage for Guarded Iteration

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 specific instance of the metalanguage and establishing soundness and (computational) adequacy for this case.

extended version for the special issue

References in corpus (7)

• Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
• Bialgebraic Semantics for Logic Programming
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Intensionality, Definability and Computation
• A Hoare logic for the coinductive trace-based big-step semantics of While
• Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion
• A Semantics for Hybrid Iteration