Redex -> Coq：迈向 Redex 归约语义可判定性理论
计算机科学中的逻辑
2024-02-07 v1 编程语言
摘要
我们提出了开发一种工具的第一步，该工具旨在将 Redex 模型自动转换为 Coq 中（有望）语义等价的模型，并提供策略以帮助验证此类模型的基本属性。这项工作在很大程度上基于 Klein 等人开发的 Redex 语义模型。通过对 Redex 中匹配问题进行简单推广，我们获得了一种适用于在 Coq 中机械化的算法，并证明了其可靠性及其与 Klein 等人提出的原始解的一致性。在此过程中，我们还调整了我们机械化工作的某些部分，以便更好地为将来纳入当前模型中尚不存在的 Redex 特性（如其 Kleene 星号算子）做好准备。最后，我们讨论了此项工作所开启的未来发展路径。
引用
@article{arxiv.2402.03488,
title = {Redex -> Coq: towards a theory of decidability of Redex's reduction semantics},
author = {Mallku Soldevila and Rodrigo Ribeiro and Beta Ziliani},
journal= {arXiv preprint arXiv:2402.03488},
year = {2024}
}