Certified Compilers à la Carte
summary
The work extends the Rocq proof assistant with a plugin called Rocqet that adds object-oriented extensibility features—late binding, mixin composition, and family polymorphism—inside a dependent-type theorem prover. It uses these features to modularize and reuse formalizations for intermediate languages, ISAs, and compiler transformations, enabling composable, certified compiler components and showing improved proof-compilation and extracted-compiler performance relative to prior extensible-metatheory approaches.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:15Certified compilers matter
- 2:39Expression problem
- 4:47Modular compiler goals
- 5:51Rocket features
- 8:00Modular compiler passes
- 9:22Rocket extensibility
- 11:11Case study: Rocket to Comet
- 12:56Rocket performance
- 13:38Future modularity
- 14:05Q&A
related talks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
34mLanguage Design Where Paradigms Meet
19mExtensible Metatheory Mechanization via Family Polymorphism
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
42mSession with the Rocq Development Team