Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language
In this paper, building on prior work of Hur et al., we develop a novel approach to compositional compiler verification based on parametric inter-language simulations (PILS). PILS are modular: they enable compiler verification in a manner that supports separate compilation. PILS are transitive: we use them to verify Pilsner, a simple (but non-trivial) multi-pass optimizing compiler (programmed in Coq) from an ML-like source language S to an assembly-like target language T, going through a CPS-based intermediate language. Pilsner is the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Lastly, PILS are flexible: we use them to additionally verify
- Zwickel, a direct non-optimizing compiler for S, and
- a hand-coded self-modifying T module, proven correct with respect to an S-level specification.
Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language.
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.
In 2015 ACM SIGPLAN International Conference on Functional Programming (ICFP 2015).
Conference Version: (paper in PDF, appendix, Coq source)