Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Sun 23 Sep 2018 11:20 - 12:00 at Frisco+Burlington Route - morning-3

In recent work, we have proposed a new axiomatic approach to unifying notions of guardedness, where the main idea is to provide an abstract notion of guardedness applicable to a wide range of (mutually incompatible) models spanning from the topos of trees to infinite-dimensional Hilbert spaces. A specific, and yet generic, instance of this notion is effectful guarded iteration.

As originally argued by Moggi, strong monads can be regarded as carriers of computational effects, and thus the arising computational metalanguage can be viewed as a generic programming language over these effects. We extend this perspective by proposing an analogous metalanguage parameterized with a notion of guardedness and equipping it with guarded iteration. In doing so, we follow the approach of Geron and Levy who already explored the case of unguarded iteration by suitably extending a fine-grain call-by-value language, a refined variant of Moggi’s language. A key ingredient we borrow from Geron and Levy’s work is the exception raising/handling mechanism, allowing for an efficient organization of while-loops via rising and iterative exception handling.

Sun 23 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

11:20 - 12:00
A Metalanguage for Guarded Iteration
Sergey Goncharov Friedrich-Alexander-Universität Erlangen-Nürnberg, Christoph Rauch FAU Erlangen-Nürnberg, Lehrstuhl 8, Lutz Schröder FAU Erlangen-Nürnberg, Lehrstuhl 8