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/
)
- 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)
$ ./build-base
Coq, MathComp and the regular language library will be rebuilt. Do you want to continue? [yes/no] YES
...
$ ./build
...
- 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)