Holcf '11: a definitional domain theory for verifying functional programs
Holcf '11: a definitional domain theory for verifying functional programs
复制标题
Holcf 11：用于验证功能程序的定义域理论
DOI：
10.15760/etd.113
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
B. Huffman
中科院分区：
文献类型：
--
作者：
J. Hook;B. Huffman
HOLCF是一个交互式定理证明系统，它使用领域理论的数学来对用函数式编程语言编写的程序进行推理。本文介绍了HOLCF '11，这是HOLCF的彻底修订和扩展版本，它推进了程序验证的最新技术：HOLCF '11可以推理许多超出其他正式证明工具范围的程序定义，同时提供高度的证明自动化。通过坚持定义方法来确保系统的可靠性：根据先前的概念定义新的常量和类型，而不引入新的公理。
HOLCF is an interactive theorem proving system that uses the mathematics of domain theory to reason about programs written in functional programming languages. This thesis introduces HOLCF '11, a thoroughly revised and extended version of HOLCF that advances the state of the art in program verification: HOLCF '11 can reason about many program definitions that are beyond the scope of other formal proof tools, while providing a high degree of proof automation. The soundness of the system is ensured by adhering to a definitional approach: New constants and types are defined in terms of previous concepts, without introducing new axioms.
Major features of HOLCF '11 include two high-level definition packages: the Fixrec package for defining recursive functions, and the Domain package for defining recursive datatypes. Each of these uses the domain-theoretic concept of least fixed points to translate user-supplied recursive specifications into safe low-level definitions. Together, these tools make it easy for users to translate a wide variety of functional programs into the formalism of HOLCF. Theorems generated by the tools also make it easy for users to reason about their programs, with a very high level of confidence in the soundness of the results.
As a case study, we present a fully mechanized verification of a model of concurrency based on powerdomains. The formalization depends on many features unique to HOLCF '11, and is the first verification of such a model in a formal proof tool.
快速而宽松的推理在道德上是正确的
影响因子：
--
作者：
Danielsson N
通讯作者：
Danielsson N