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.
Hugo Paquet;Philip Saville, 2023, Effectful Semantics in 2-Dimensional Categories: Premonoidal and Freyd Bicategories, arXiv (Cornell University), 397, pp. 190-209, 10.4204/eptcs.397.12.
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.
Damiano Mazza;Luc Pellissier;Pierre Vial, 2017, Polyadic approximations, fibrations and intersection types, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-28, 10.1145/3158094, https://doi.org/10.1145/3158094.