-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2019.VerifiedCompilation
Nachi edited this page Jun 2, 2020
·
4 revisions
by Alexander Fuhs
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.
- 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)