Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
summary
A Coq framework for modular, extensible compiler verification that proves an inductive equivalence preservation theorem so adding one feature requires one new compilation case and one new proof obligation. It represents languages as sorted equational theories, uses a Galina script to generate substitution lemmas, and an unverified evaluator plus a verified proof checker to discharge many goals automatically; most case-study passes are proved automatically. Demonstrated by a multipass STLC→CPS→closure conversion pipeline that extends with naturals, unit, fix, heap while reusing prior proofs.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:26Context
- 1:31Long-Term Goals
- 2:15Core Theory
- 3:54Continuation-Passing Style (CPS)
- 6:16Type and Equivalence Preservation: Linking
- 7:02Type and Equivalence Preservation Is Enough
- 8:30Proving Preservation
- 9:47Extension: Recursive Functions
- 12:01Extending the Proof of Preservation
- 12:35The Preserving Predicate
- 14:35Current Case Study
- 15:27Substitution and Naming
- 16:55Automation in Pyrosome: Substitution
- 17:54Automation in Pyrosome: Reduction
- 21:12Ongoing/Future Work
- 29:00Optimizations
related talks
16mPyrosome: Verified Compilation for Modular Metatheory
19mExtensible Metatheory Mechanization via Family Polymorphism
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
19mCertified Compilers à la Carte
15mCompiling with Continuations, Correctly
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
29mTowards Formally Verified Just-In-Time Compilation
01h 06mVerifying a compiler through equational means