编程语言语义中的定理证明支持

我们将简单编程语言的语义描述为归纳构造演算中的形式文档，并可由 Coq 证明系统进行验证。涵盖的方面包括自然语义、指称语义、公理语义和抽象解释。在适当的情况下还提供了递归函数描述，从而生成一个验证条件生成器和一个静态分析器，可在定理证明器内部运行以用于反射式证明。此外还描述了从指称语义中提取解释器的过程。所有不同方面均被形式化地证明相对于自然语义规范是可靠的。