Re: [Caml-list] equivalent checking of ocaml program?

[Robert Jakob <rj@robertjakob.de>]

On Mon, 30 Sep 2013 17:49:11 +0200
Gabriel Scherer <gabriel.scherer@gmail.com> wrote:

> This thread may be a good opportunity to advertize for some work on
> static program verification that has been applied to OCaml (sadly, it
> is actually quite rare to see program verification efforts for
> functional programming languages, in large part because funding
> bodies and reviewers appreciate applications to mainstream language
> with larger codebases). I am aware of the following, feel free to add
> more suggestions:
> - MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/
>   Based on foundational work on model-checking of higher-order
> programs by Ong, Kobayashi and others (see the citations of the
> papers on the webpage), MoCHi can work with a subset of OCaml. It is
> not ready to handle real-world programs, both in term of verification
> time and the ocaml feature it understands, but going in the right
> direction -- and the underlying tools are rapidly improving, see e.g.
> the recent work on C-SHORe
The approaches by Ong, Kobayashi, Broadbent et al. work on higher-order
recursion schemes (HORS) to represent output/states of functional
programs. Yet, it is not known if the equivalence of two HORS is
decidable. So this might be applicable to deciding the equivalency of
ocaml programs (wrt. outputs/state), but it is not clear.

r.