Demo of Intrinsically Typed Compilation of Imperative Code in Agda

Arjen Rouvoet

I’ve been working on using the framework that we developed for intrinsically typed interpretation of linear language (CPP ‘20) to get compositional typesafe compilation of an imperative language. The key idea being that we can model label binding in JVM bytecode using these ‘proof relevant separation algebras’ that also powered our previous work. In this demo I hope to give you an idea of how this works and I hope to gain some insight into how I may explain it on paper.

---

Previous: Jeff Smits | Gradual Types for Stratego - Demo Edition
Next: Robbert Krebbers | Proving Semantic Type Soundness in Iris