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.

Material from talk

• Slides here
• Repository with the source code of thesis here (alternatively, updated version here)

References

• Alexander Fuhs. 2020. Verified Compilation to Intrinsically Typed Control-Flow Graphs in Agda (https://github.com/InitialTypes/Club/blob/master/lectures/verified-compilation-cfg/MasterThesis.pdf)
• Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers and Eelco Visser. 2017. Intrinsically-typed definitional interpreters for imperative languages (http://casperbp.net/papers/intrinsicallytyped.html)