Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala. Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. In Ranjit Jhala, Isil Dillig, editors, PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. pages 918-933, ACM, 2022. [doi]
Abstract is missing.