Translation validation of a pattern-matching compiler - Archive ouverte HAL Access content directly
Conference Papers Year :

Translation validation of a pattern-matching compiler

(1) , (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.
Fichier principal
Vignette du fichier
pattern-checking-workshop-paper.pdf (203.28 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03145030 , version 1 (18-02-2021)


  • 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⟩
44 View
44 Download


Gmail Facebook Twitter LinkedIn More