COPLAS talk: Ahmad Al-Sibahi
Verification of High-Level Transformations with Inductive Refinement Types
Speaker: Ahmad Al-Sibahi, University of Copenhagen and skanned
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference) showing that we can effectively verify stated properties.
This is joint work with Thomas Jensen, Aleksandar Dimovski and Andrzej Wąsowski to be presented at GPCE 2018.
Ahmad Al-Sibahi obtained his Ph.D. in computer science from the IT University of Copenhagen. He is presently employed as researcher at skanned and enrolled as postdoc at DIKU, the Department of Computer Science, University of Copenhagen, working on probabilistic programming.
All are welcome. No registration required.