Merge Sort in Coq

An example of using the Coq language to generate a simple but practical formally verificated sorting algorithm

HowTo

Regenerate Makefile:

$ coq_makefile -f _CoqProject -o Makefile

or

$ make Makefile.conf

clean project:

$ make clean
# or even
$ make cleanall

build coq file:

$ make ${FILE_NAME}.vo

build all:

$ make

build and run OCaml code with generated by GenOcaml.v implementation of merge_sort function:

$ make
$ cd ocaml
$ make run

clean OCaml code:

# in /ocaml dir
$ make clean

Run generated code as F# here