Formalizing Higher-Order Termination in Coq
Logic in Computer Science
2021-12-14 v2
Abstract
We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.
Keywords
Cite
@article{arxiv.2112.05715,
title = {Formalizing Higher-Order Termination in Coq},
author = {Deivid Vale and Niels van der Weide},
journal= {arXiv preprint arXiv:2112.05715},
year = {2021}
}