Extracting Imperative Programs from Proofs: In-place Quicksort

Extracting Imperative Programs from Proofs: In-place Quicksort
复制标题

从证明中提取命令式程序：就地快速排序

DOI：
--
复制
发表时间：
2013
期刊：
Types for Proofs and Programs
影响因子：
--
通讯作者：
Gregory J. M. Woods
Gregory J. M. Woods
中科院分区：
--
文献类型：
--
作者：
Ulrich Berger;M. Seisenberger;Gregory J. M. Woods

文献摘要

被引文献

相似文献

程序提取的过程主要与 函数式程序，较少关注命令式程序提取。在本文中，我们考虑一个标准的问题，命令式编程：就地快速排序。我们形式化的证明，每一个自然数数组可以排序，并适用于实现 解释从证明中提取程序。使用单子，我们 能够表现出被提取的内在的命令性质， 程序.我们认为这是自动提取命令式程序的第一步。案例研究是在交互式证明助手Minlog中进行的。
The process of program extraction is primarily associated with functional programs with less focus on imperative program extraction. In this paper we consider a standard problem for imperative programming: In-place Quicksort. We formalize a proof that every array of natural numbers can be sorted and apply a realizability interpretation to extract a program from the proof. Using monads we are able to exhibit the inherent imperative nature of the extracted program. We see this as a first step towards an automated extraction of imperative programs. The case study is carried out in the interactive proof assistant Minlog.