A metalanguage for guarded iteration

Goncharov S, Rauch C, Schröder L (2021)

Publication Language: English

Publication Type: Journal article, Original article

Publication year: 2021

Journal

Theoretical Computer Science Elsevier

DOI: 10.1016/j.tcs.2021.04.005

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.

Authors with CRIS profile

Sergey Goncharov Lehrstuhl für Informatik 8 (Theoretische Informatik) Christoph Rauch Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik)

How to cite

APA:

Goncharov, S., Rauch, C., & Schröder, L. (2021). A metalanguage for guarded iteration. Theoretical Computer Science. https://doi.org/10.1016/j.tcs.2021.04.005

MLA:

Goncharov, Sergey, Christoph Rauch, and Lutz Schröder. "A metalanguage for guarded iteration." Theoretical Computer Science (2021).

BibTeX: Download