Redex -> Coq: towards a theory of decidability of Redex's reduction semantics

Mallku Soldevila, Rodrigo Ribeiro, Beta Ziliani

We propose the first steps in the development of a tool to automate the translation of Redex models into a (hopefully) semantically equivalent model in Coq, and to provide tactics…