Abstracts.2019.VerifiedCompilation

Verified Compilation to Intrinsically Typed Control-Flow Graphs in Agda

by Alexander Fuhs

Abstract

In this talk I will present my master thesis about a verified compilation pass from a while language to a control-flow graph representation in which labels are represented by de Bruijn indices. Both the while language and the control-flow graph representation are defined by an intrinsically typed syntax which incorporates the type system into the abstract syntax.

Slides here.

References

Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers and Eelco Visser. 2017. Intrinsically-typed definitional interpreters for imperative languages https://dl.acm.org/doi/10.1145/3158104