一句话：提出用 Haskell 子集和抽象单子编写可复用的指令集语义，以同一核心语义支持测试、交互证明与软硬件模型检测。
指令集形式语义是众多验证、合成、编程与调试工具的基础，但不同工具对语义的使用方式差异很大。已有跨工具复用方案多依赖 Sail 等面向指令集领域的专用语言与翻译工具。本文以开放 RISC-V 指令集族为背景，探索另一种路径：用精心选取的 Haskell 子集编写语义，不引入新的语言翻译器，而是通过类型类实例对语义进行参数化；借助 monad 及其抽象，同一核心语义可服务多种用途。作者展示了用该核心语义支持软件与硬件的测试、交互式证明和模型检测，表明 monad 与类型类抽象能支持便捷的 ISA 语义原型开发。
Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use semantics in rather different ways. The best-known work applying single semantics across diverse tools relies on domain-specific languages like Sail, where the language and its translation tools are specialized to the realm of instruction sets. In the context of the open RISC-V instruction-set family, we decided to explore a different approach, with semantics written in a carefully chosen subset of Haskell. This style does not depend on any new language translators, relying instead on parameterization of semantics over type-class instances. We have used a single core semantics to support testing, interactive proof, and model checking of both software and hardware, demonstrating that monads and the ability to abstract over them using type classes can support pleasant prototyping of ISA semantics.
@article{paperbot1928,
title = {Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)},
author = {Thomas Bourgeat and Ian Clester and Andres Erbsen and Samuel Gruetter and Pratap Singh and Andy Wright and Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607833}
}