Posted by Jesper on January 7, 2021
Back in 2019, I wrote two posts about user-definable rewrite rules in Agda (which have since then been rewritten into a TYPES paper) and promised a third one about how to make rewrite rules safe to use (or at least safer). At the time, I was hard at work together with Théo Winterhalter and Nicolas Tabareau from the Galinette group in Nantes to tackle the problem of checking safety of rewrite rules, and in particular trying to ensure subject reduction holds. Little did we know that the problem would turn out a lot trickier than I expected, so much that we did not make it in time for the ICFP 2020 deadline.
However, now I am very glad to say our paper The Taming of the Rew: A Type Theory With Computational Assumptions is to appear at POPL 2021 on January 20, in less than two weeks time.
In fact, you can already read the paper
as well as watch our talks (one 5 minute version by Théo and one 30 minute version by Théo and me). So in case you were still waiting for that post, go ahead and watch the talks or read the paper. And remember, when you do --rewriting in Agda don’t forget to also --confluence-check!