Adapting functional programs to higher order logic
Adapting functional programs to higher order logic
复制标题
使函数式程序适应高阶逻辑
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Konrad Slind
中科院分区：
文献类型：
--
作者：
Scott Owens;Konrad Slind
高阶逻辑证明系统将函数式编程与逻辑相结合，为函数式程序员提供了程序、规范和证明形式化的舒适设置。然而，在这种环境中工作的一个可能不熟悉的方面是，正式建立程序终止是必要的。在许多情况下，终止可以自动证明，但也有一些有用的发散程序和其他总是终止但难以终止证明的程序。我们将讨论支持诸如逻辑函数之类的程序表达式的技术。
Higher-order logic proof systems combine functional programming with logic, providing functional programmers with a comfortable setting for the formalization of programs, specifications, and proofs. However, a possibly unfamiliar aspect of working in such an environment is that formally establishing program termination is necessary. In many cases, termination can be automatically proved, but there are useful programs that diverge and others that always terminate but have difficult termination proofs. We discuss techniques that support the expression of such programs as logical functions.