2022.02.28
Abstract
Building these models is challenging, requiring experimen- tation, dialogue with vendors or standards bodies, and validation;
这里极度缺乏“dialogue with vendors or standards bodies”， 比较缺乏validation。
Lem definitions are translatable into
- OCaml for testing
- Coq, HOL4, and Isabelle/HOL for proof
- LaTeX and HTML for presentation
Intro
各个领域（体系结构、编程语言、协议）语义严谨化的相关工作。
已有语义模型不兼容，重复工作多。
相关工作：
- 通用编程语言：……
- 验证器语言：……，分裂、难以精通
- 已有工作建立各个验证器的内在联系[1, 12-15, 39]
Lem in practice
- [30] IBM and ARM relaxed-memory behaviour
- [3] C/C++11 memory model and concurrency model
- [4, 31] Power and C/C++11
- [21] Power
- [6] TCP/IP
- [25] Ott
- [18] ML on X64
- C
- ...