Cartesian closed 2-categories and permutation equivalence in
higher-order rewritingArticle
Authors: Tom Hirschowitz
0000-0002-7220-4067
Tom Hirschowitz
We propose a semantics for permutation equivalence in higher-order rewriting.
This semantics takes place in cartesian closed 2-categories, and is proved
sound and complete.
Benedikt Ahrens;André Hirschowitz;Ambroise Lafont;Marco Maggesi, 2019, Reduction monads and their signatures, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-29, 10.1145/3371099, https://doi.org/10.1145/3371099.