Language Design Where Paradigms Meet
summary
A new language called rocket extends rock with object‑oriented abstractions so inductive types and proofs are open inductive types that late‑bind constructors and let traits add cases without recompilation. A type‑preserving compilation uses wellfounded open recursion to avoid cycles and preserve Coq‑style consistency, and trait composition auto‑synthesizes proofs so a nanopass setup (four ILs, three passes) fuses into a single traversal — demonstrated by refactors of CompCert front/back ends and a RISC‑V ISA model using nanopass fusion.
AI-written summary · about
chapters (26)
- 0:00Language design at paradigms' intersection
- 1:46Modular proof composition challenge
- 3:31Expression problem in mechanized proofs
- 7:03Proof systems and OO ideas
- 8:06Rocket language design
- 8:47Mechanizing STLC in Rock
- 10:11STLC with recursive functions
- 11:36Rocket traits for modular extensions
- 13:03Proof reuse without recompilation
- 14:05Proof systems vs extensibility
- 14:30Closed vs open inductive types
- 15:35Family polymorphism for open types
- 17:45Definitional unfolding and equalities
- 18:51Reasoning without unfolding
- 20:19Open recursion and consistency
- 21:25Type-preserving translation to Rock
- 22:29Well-founded open recursion
- 24:58Expression problem solved
- 25:19Extensible verified compiler
- 26:45Modularity in compiler passes
- 28:09Nanopass fusion with Rocket traits
- 29:15Refactoring CompCert
- 29:57Modularity across compiler pipelines
- 30:40Open challenges in Rocket
- 31:00Paradigm fusion reflections
- 32:25Q&A on Rocket
related talks
19mCertified Compilers à la Carte
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
21mNested Inductive Types for Rocq and Lean
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
51mElpi: rule-based meta-languge for Rocq
19mExtensible Metatheory Mechanization via Family Polymorphism
16mPyrosome: Verified Compilation for Modular Metatheory
45mLanguage-Oriented Programming with Racket