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

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]

@inproceedings{Pit-ClaudelPJEC22,
  title = {Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code},
  author = {Clément Pit-Claudel and Jade Philipoom and Dustin Jamner and Andres Erbsen and Adam Chlipala},
  year = {2022},
  doi = {10.1145/3519939.3523706},
  url = {https://doi.org/10.1145/3519939.3523706},
  researchr = {https://researchr.org/publication/Pit-ClaudelPJEC22},
  cites = {0},
  citedby = {0},
  pages = {918-933},
  booktitle = {PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022},
  editor = {Ranjit Jhala and Isil Dillig},
  publisher = {ACM},
  isbn = {978-1-4503-9265-5},
}