Program Extraction for Mutable Arrays

By Kazuhiko Sakaguchi

This repository provides a novel, lightweight, and axiom-free method for verification and extraction of efficient effectful programs which use mutable arrays. Our method consists of the following three parts:

• Improved Extraction Plugin for Coq (see coq-mod submodule)
• Modified Mathematical Components (MathComp) Library (see math-comp-mod submodule)
• Small Monadic DSL for Mutable Array Programming --- The Array State Monad (see theories/marray/)

Requirements

• OPAM, OCaml 4.07.0+flambda, Camlp5, Ocamlbuild and ocamlfind
• tmux and zsh (for benchmark tools and build scripts)

Following materials are also required, but included as submodules or automatically downloaded by the build script.

• Coq (official version 8.8.0 and extraction-efficient-finfun-master branch)
• Mathematical Components Library (official version 1.7.0 and modified-fintype branch)
• Constructive Regular Language Library (updated 2013-12-07, apply regular.patch)

How to Build

$ ./build-base
Coq, MathComp and the regular language library will be rebuilt. Do you want to continue? [yes/no] YES
...
$ ./build
...

References

• Kazuhiko Sakaguchi. Program Extraction for Mutable Arrays. FLOPS 2018.
• Kazuhiko Sakaguchi and Yukiyoshi Kameyama. Efficient Finite-Domain Function Library for the Coq Proof Assistant. IPSJ Transactions on Programming, Vol 10, No 1, pp. 14-28, 2017.
• 坂口和彦 (2016)「Coq による定理証明 2016.12」 Tsukuba Coq Users' Group. (web page)
• 坂口和彦 (2015)「Coq による定理証明 2015.12」 Tsukuba Coq Users' Group. (web page)