Checking confluence of rewrite rules in Agda

Jesper Cockx

Dependently typed languages provide strong guarantees of correctness for our programs and proofs, but they can be hard to use and extend. To increase their practicability and expressivity, they can be extended with user-defined rewrite rules. However, this is dangerous as it is very easy to break expected good properties of these systems, e.g., termination, confluence, canonicity or subject reduction [3]. Among those, confluence is a key ingredient to retain subject reduction and as such is essential.

In this talk, I will present a new criterion for checking confluence of user-defined rewrite rules in the Agda language. Our criterion is based on the classic proof of confluence of lambda calculus by Tait and Martin-Löf, but extends it to arbitrary higher-order and potentially non-terminating rewrite rules.

---

Previous: Arjen Rouvoet | Discussion about shoulders of giants: related work in research and writing
Next: Lucas Escot | Univalent Parametricity for Programming Modulo Equivalences