Program Extraction for Mutable Arrays
Program Extraction for Mutable Arrays
复制标题
可变数组的程序提取
DOI：
10.1007/978-3-319-90686-7_4
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Kazuhiko Sakaguchi
中科院分区：
文献类型：
--
作者：
Cyril Cohen;Kazuhiko Sakaguchi;Enrico Tassi;Kazuhiko Sakaguchi
我们提出了一种轻量级方法来表示、验证和提取 Coq 证明助手中涉及可变数组的高效程序。我们的方法主要由一个用于处理可变数组的库和一个改进的提取插件组成。我们的库提供了一种用于对涉及可变数组的建模计算的一元域特定语言、一种基于 Ssreflect 扩展和数学组件库的简单推理方法，以及一种使用就地更新的高效 OCaml 程序的提取方法。我们的提取插件提高了提取程序的性能，或者更恰当地说，通过对纯函数式程序应用简单的程序转换，它减少了归纳和共归纳对象的构造和销毁成本以及函数调用成本。作为我们方法的具体应用，我们提供了并查数据结构和快速排序算法的高效实现、正确性证明和基准。
We present a lightweight method to represent, verify, and extract efficient programs involving mutable arrays in the Coq proof assistant. Our method mainly consists of a library for handling mutable arrays and an improved extraction plugin. Our library provides a monadic domain specific language for modeling computations involving mutable arrays, a simple reasoning method based on the Ssreflect extension and the Mathematical Components library, and an extraction method to efficient OCaml programs using in-place updates. Our extraction plugin improves the performance of our extracted programs, or more appropriately, through the application of simple program transformations for purely functional programs, it reduces both construction and destruction costs of inductive and coinductive objects and function call costs. As concrete applications for our method, we provide efficient implementations, correctness proofs, and benchmarks of the union–find data structure and the quicksort algorithm.