Pyrosome: Verified Compilation for Modular Metatheory
summary
Pyrosome is a Coq framework that defines languages as lists of inference rules (GATs) and treats program equivalence as the reflexive‑transitive‑symmetric congruence closure of those equations, so proofs are monotonic under language extension. Correctness is type and equivalence preservation proved by an inductive preserving predicate that adds one case per rule, enabling incremental verification and vertical composition of compilers. Case study: a multipass compiler from STLC→System F with simple references through CPS and closure conversion, supporting open programs (linking) and heavy proof automation (127 goals, 110 automatic).
AI-written summary · about
chapters (12)
- 0:00Pyrosome introduction
- 1:03Compiler correctness for extensions
- 3:53Pyrosome formalism
- 5:37Type and equivalence preservation
- 7:23Extensible proofs
- 8:51CPS compiler case study
- 9:54Adding recursive functions
- 10:35Polymorphism support
- 11:57Diverse language cases
- 12:40Future work and lower languages
- 13:01Q&A on ergonomics
- 14:27Q&A on optimizations
related talks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
19mExtensible Metatheory Mechanization via Family Polymorphism
15mCompiling with Continuations, Correctly
15mSulfur: Substitution Generation using a Logical Framework
34mLanguage Design Where Paradigms Meet
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
12mOn the metatheory of IRs and the CPS-calculus
19mCertified Compilers à la Carte