Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq

Jens de Waard (TU Delft PL)

For software developers, any non-trivial program quickly grows to a scope where it is difficult to ascertain whether the program actually does what the programmer intended. There have been several solutions for this problem, such as writing tests that automatically assert facts about the execution of the program. Another approach is the writing of abstract interpreters that analyze the system under test for properties such as type safety. Proving these abstract interpreters to be sound and correct is cumbersome and often omitted.

To ease the development of such proofs, prior work has shown that these proofs can be decomposed into smaller, independent lemmas from which the soundness of the entire interpreter follows due to the abstract and concrete interpreters being instantiations of a shared interpreter. This work is now being implemented using the Coq proof assistant in order to develop a framework that may aid in the writing of soundness proofs for existing interpreters.

---

Previous: | Oracle funds Flexible, Composable, and Incremental Compiler Pipelines
Next: Simon Fowler | Exceptional Asynchronous Session Types: Session Types without Tiers