Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. pages 167-181, ACM, 2023. [doi]
Abstract is missing.