Prosecco Seminar - SyTeCi: Automating contextual equivalence for higher-order programs with references
SyTeCi: Automating contextual equivalence for higher-order programs with references
Guilhem Jaber, Université de Nantes
This talk will present SyTeCi, the first general automated tool to check contextual equivalence for programs written in RefML, a higher-order language with references (i.e. local mutable states), corresponding to a fragment of OCaml. After introducing the notion of contextual equivalence, we will see on some examples why it is hard to prove such equivalences (reentrant calls, private state). We will sketch a trace model capturing exactly contextual equivalence (i.e. being fully abstract) for RefML, based on a operational reformulation of game semantics.
Then, we will introduce SyTeCi, a tool to automatically check such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of reachability of “error states” in transition systems of memory configurations. Soundness and completeness of this reduction rely crucially on the fully abstract trace model of RefML.
Contextual equivalence being undecidable (even in a finitary setting), so does the non-reachability problem for such transition systems. However, under some restrictions, it is possible to restate the non-reachability problem into a satisfiability problem for constrained Horn clauses. We will then present a prototype implementing these ideas, that can prove automatically many non-trivial examples of the literature, that could only be proved by hand before.
Finally, we will end this talk by presenting directions to extend this work to a language with polymorphism.