Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
Tom Hirschowitz (CNRS, Universit\'e de Savoie)
TL;DR
This paper introduces a semantics for permutation equivalence in higher-order rewriting using cartesian closed 2-categories, establishing soundness and completeness for this approach.
Contribution
It provides a novel semantic framework for permutation equivalence in higher-order rewriting based on cartesian closed 2-categories, with formal proofs of soundness and completeness.
Findings
Semantics for permutation equivalence in higher-order rewriting established
Soundness and completeness of the semantics proved
Framework based on cartesian closed 2-categories
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.