Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.

Clment Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala

Browse the full PLDI paper archive.