Session with the Rocq Development Team
summary
Rocq releases 9.0 and 9.1 ship a single rag binary, a split of the standard library into a minimal core plus a separate stdlib, and fixes to the guard checker and delta resolvers that were causing soundness and equivalence bugs. New features include sort polymorphism, Ltac2 and notation extensions, relocatable installs, extraction supporting subpolymorphic defs, Docker CI/docs, eliminators for nested inductives, polymorphic rewriting across sorts, automatic goal naming, and a push toward algebraic universes with a verified constraint solver and experimental rewrite-based definitional equality.
AI-written summary · about
chapters (6)
- 0:00Welcome to Rocq workshop
- 1:11Rocq 9.0 and 9.1 updates
- 7:16Rocq 2026 features teaser
- 13:16Future of Rocq: universe and type theory
- 20:41Verified compilation projects
- 23:11Q&A with Rocq team
related talks
44mSession with the Coq Development Team
46mSession with the Coq Development Team
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
19mCertified Compilers à la Carte
51mElpi: rule-based meta-languge for Rocq
34mLanguage Design Where Paradigms Meet
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
31mThe R7RS-Large Roadmap (Invited Talk)