Embedding Untrusted Imperative ML Oracles into Coq Verified Code

This preprint has been largely rewritten and integrated into Sylvain Boulm{\'e}'s Habilitation in 2021, See http://www-verimag.imag.fr/~boulme/hdr.html.This paper investigates a lightweight approach-combining Coq and OCaml typecheckers-in order to formally verify higher-order imperative programs in partial correctness. In this approach, the user does never formally reason about effects of imperative functions, but only about their results. Formal guarantees are obtained by combining parametric reasoning over polymorphic functions (i.e. "theorems for free" a la Wadler) with verified defensive programming. This paper illustrates the approach on several examples. Among them: first, the certification of a polymorphic memoized fixpoint operator using untrusted hash-tables; second, a certified Boolean SAT-solver, invoking internally any untrusted but state-of-the-art SAT-solver (itself generally programmed in C/C++)