A Metalanguage for Guarded Iteration


By Sergey Goncharov, Friedrich-Alexander-Universität Erlangen-Nürnberg.

Abstract. Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. To formalize this, a unified axiomatic notion of guardedness in symmetric monoidal categories emerged recently, covering various examples from program semantics, process algebra, hybrid computations and beyond -- the list is being completed on an on-going basis. Here, I present a metalanguage for guarded iteration based on combining axiomatic guardedness with the popular fine-grain call-by-value paradigm, intended as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. I give a generic (categorical) semantics for 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 by providing a corresponding adequacy result..

About the Speaker. Sergey Goncharov is a senior lecturer (german: Akademischer Oberrat) at Friedrich-Alexander-Universität Erlangen-Nürnberg. He received his bachelor and master degrees in applied mathematics and computer science respectively in the Taras Shevchenko National University of Kyiv, and subsequently his PhD degree in computer science in the University of Bremen, honored with the highest academic degree (summa cum laude). Since recently, he is holding the habilitation post-doctoral qualification, obtained at the current place of employment. His interests are mainly concentrated at semantic modeling of various computational phenomena for programming and verification, including statefulness, probability, nondeterminism and divergence, by making a significant use of the language and tools of category theory..


Address:  University of Minho, Gualtar campus, Braga, Portugal.

Building. Departamento de Informatica, Building 07.

Coffee session: at  1:45PM-2PM, Auditorium A2, 1st floor.

Talks session: at 2PM-3PM, Auditorium A2, 1st floor.