Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Thu 27 Aug 2020 15:45 - 16:10 at ML - Session 2

We propose an algorithm for the translation validation of a pattern matching compiler for a small subset of the OCaml pattern matching features. Given a source program and its compiled version the algorithm checks wheter the two are equivalent or produce a counter example in case of a mismatch.

Our equivalence algorithm works with decision trees. Source patterns are converted into a decision tree using matrix decomposition. Target programs, described in a subset of the Lambda intermediate representation of the OCaml compiler, are turned into decision trees by applying symbolic execution.

Translation validation of a pattern-matching compiler (ml2020-final96.pdf)203KiB