Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.

Benjamin Grgoire, Jean-Christophe Lchenet, Enrico Tassi

Browse the full CPP paper archive.