Proof-producing synthesis of ML from higher-order logic
Proof-producing synthesis of ML from higher-order logic
复制标题
从高阶逻辑对 ML 进行证明综合
DOI：
10.1145/2364527.2364545
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Myreen M
中科院分区：
文献类型：
--
作者：
Myreen M
在证明助手中发现的高阶逻辑，如Coq和各种HOL系统，为纯函数程序的开发和验证提供了方便的设置。然而，为了有效地运行这些程序，必须将它们转换（或“提取”）为编程语言（如ML或Haskell）中的函数程序。与目前的技术，这一步，这必须是值得信赖的，涉及到类似的外观对象，有非常不同的语义定义，如逻辑的集合理论模型和操作语义的编程语言。在本文中，我们展示了如何增加可信度的这一步的自动化技术。给定一个功能程序表示在高阶逻辑，我们的技术提供了相应的程序定义的操作语义的功能语言，它提供了一个机械检查定理有关的两个。这个定理然后可以被用来转移验证的属性的逻辑函数的program.We实现了我们的技术在HOL4定理prover，翻译功能的标准ML的核心子集，并已将其应用到例子，包括功能的数据结构，解析器生成器，加密算法，和垃圾收集器。
The higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of pure functional programs. However, to efficiently run these programs, they must be converted (or "extracted") to functional programs in a programming language such as ML or Haskell. With current techniques, this step, which must be trusted, relates similar looking objects that have very different semantic definitions, such as the set-theoretic model of a logic and the operational semantics of a programming language.In this paper, we show how to increase the trustworthiness of this step with an automated technique. Given a functional program expressed in higher-order logic, our technique provides the corresponding program for a functional language defined with an operational semantics, and it provides a mechanically checked theorem relating the two. This theorem can then be used to transfer verified properties of the logical function to the program.We have implemented our technique in the HOL4 theorem prover, translating functions to a core subset of Standard ML, and have applied it to examples including functional data structures, a parser generator, cryptographic algorithms, and a garbage collector.
登录
查看更多内容
用于非纯函数语言的经过验证的编译器
DOI：
--
发表时间：
2010
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
Miller-Rabin 概率素性测试的验证
DOI：
--
发表时间：
2003
期刊：
J. Log. Algebraic Methods Program.
影响因子：
--
作者：
Joe Hurd
通讯作者：
Joe Hurd
使函数式程序适应高阶逻辑
DOI：
--
发表时间：
2008
期刊：
High. Order Symb. Comput.
影响因子：
--
作者：
Scott Owens;Konrad Slind
通讯作者：
Konrad Slind
使用 PLT Redex 进行语义工程
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
M. Felleisen;R. Findler;M. Flatt
通讯作者：
M. Flatt
HOL 开发主线
DOI：
--
发表时间：
2002
期刊：
Computer/law journal
影响因子：
--
作者：
Michael Norrish;Konrad Slind
通讯作者：
Konrad Slind