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 to help in the certification of fundamental properties of such models. The work is heavily based on a model of Redex's semantics developed by Klein et al. By means of a simple generalization of the matching problem in Redex, we obtain an algorithm suitable for its mechanization in Coq, for which we prove its soundness properties and its correspondence with the original solution proposed by Klein et al. In the process, we also adequate some parts of our mechanization to better prepare it for the future inclusion of Redex features absent in the present model, like its Kleene-star operator. Finally, we discuss future avenues of development that are enabled by this work.

翻译：我们提出了开发工具的第一步，旨在将Redex模型自动转化为（期望）在Coq中语义等价的模型，并提供策略以辅助认证此类模型的基本性质。该工作紧密基于Klein等人提出的Redex语义模型。通过对Redex中匹配问题的简单泛化，我们获得了一种适合在Coq中机械化的算法，并证明了其正确性以及与Klein等人原始解决方案的对应性。在此过程中，我们还调整了部分机械化设计，使其更便于未来纳入当前模型中尚未包含的Redex特性（如Kleene星号运算符）。最后，我们讨论了此项工作所开辟的未来发展方向。