一句话：为 Rocq 引入晚绑定、mixin 组合与族多态的扩展机制（Rocqet 插件），使 CompCert 级别的认证编译器可模块化、可复用、按需组合。
认证编译器是复杂软件系统，像其他大型系统一样需要模块化、可扩展的设计。尽管可扩展元理论的机器化已取得进展，但将可扩展性与复用扩展到满足完整编译器验证的需求仍是重大挑战。本文通过为证明语言引入新的表达力来应对该挑战：其语言设计为 Rocq 证明助手配备了一种受面向对象思想（晚绑定、mixin 组合与族多态）启发的扩展机制，并以名为 Rocqet 的插件形式实现。作者进一步提出了利用 Rocqet 新表达力将 CompCert 这类大型认证开发的单体式设计模块化的策略。其收益体现在中间语言、指令集架构、编译器变换与编译器扩展的形式化中获得高度模块化与复用，并能够将这些可复用组件组合起来——即按需装配的认证编译器。论文报告证明编译性能相比先前可扩展元理论机器化工作有显著提升，同时抽取出的编译器性能良好。
Certified compilers are complex software systems. Like other large systems, they demand modular, extensible designs. While there has been progress in extensible metatheory mechanization, scaling extensibility and reuse to meet the demands of full compiler verification remains a major challenge. We respond to this challenge by introducing novel expressive power to a proof language. Our language design equips the Rocq prover with an extensibility mechanism inspired by the object-oriented ideas of late binding, mixin composition, and family polymorphism. We implement our design as a plugin for Rocq, called Rocqet. We identify strategies for using Rocqet’s new expressive power to modularize the monolithic design of large certified developments as complex as the CompCert compiler. The payoff is a high degree of modularity and reuse in the formalization of intermediate languages, ISAs, compiler transformations, and compiler extensions, with the ability to compose these reusable components—certified compilers à la carte. We report significantly improved proof-compilation performance compared to earlier work on extensible metatheory mechanization. We also report good performance of the extracted compiler.
@article{paperbot3125,
title = {Certified Compilers à la Carte},
author = {Oghenevwogaga Ebresafe and Ian Zhao and Ende Jin and Arthur Bright and Charles Jian and Yizhou Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729261}
}