Skip to Main content Skip to Navigation
Conference papers

Translation validation of a pattern-matching compiler

Francesco Mecca 1 Gabriel Scherer 2
2 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Thursday, February 18, 2021 - 9:25:36 AM
Last modification on : Saturday, May 1, 2021 - 3:41:02 AM
Long-term archiving on: : Wednesday, May 19, 2021 - 6:27:36 PM


Files produced by the author(s)


  • HAL Id : hal-03145030, version 1


Francesco Mecca, Gabriel Scherer. Translation validation of a pattern-matching compiler. ML Family Workshop, Aug 2020, New Jersey /Online, United States. ⟨hal-03145030⟩



Les métriques sont temporairement indisponibles