Abstract Interpreters: a Monadic Approach to Modular Verification
This program is tentative and subject to change.
We argue that monadic interpreters built as layers of interpretations stacked atop the free monad constitute a promising way to implement and verify abstract interpreters in dependently-typed theories such as the one underlying the Coq proof assistant.
The approach enables modular proofs of soundness of the resulting interpreters. We provide generic abstract control flow combinators proven correct once and for all against their concrete counterpart. We demonstrate how to relate concrete handlers implementing effects to abstract variants of these handlers, essentially capturing the traditional soundness of transfer functions in the context of monadic interpreters. Finally, we provide generic results to lift soundness statements via the interpretation of stateful and failure effects.
We formalize all the aforementioned combinators and theories in Coq, and demonstrate their benefits by implementing and proving correct two illustrative abstract interpreters for a structured imperative language and a toy assembly.
This program is tentative and subject to change.
Tue 3 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Algebraic and Computational EffectsICFP Papers and Events / JFP First Papers | ||
10:30 18mTalk | Abstracting Effect Systems for Algebraic Effect Handlers ICFP Papers and Events Takuma Yoshioka Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University | ||
10:48 18mTalk | Parallel Algebraic Effect Handlers ICFP Papers and Events Ningning Xie University of Toronto, Daniel D. Johnson Google Research, Dougal Maclaurin Google DeepMind, Adam Paszke Google Research | ||
11:06 18mTalk | Abstract Interpreters: a Monadic Approach to Modular Verification ICFP Papers and Events Sébastien Michelland Université Grenoble-Alpes, Grenoble INP, LCIS, Yannick Zakowski Inria, Laure Gonnord Univ. Grenoble Alpes, Grenoble INP, LCIS, Valence, France DOI Pre-print | ||
11:24 18mTalk | Algebraic effects and handlers for arrowsJFP First Paper JFP First Papers | ||
11:42 18mTalk | How to Bake a Quantum $\Pi$ ICFP Papers and Events Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University |