@inproceedings{seo-2024-correctly,
  doi = {10.4230/LIPICS.ITP.2024.33},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.33},
  author = {Seo, Audrey and Lam, Christopher and Grossman, Dan and Ringer, Talia},
  keywords = {proof transformations, compiler validation, program logics, proof engineering, Theory of computation → Logic and verification, Theory of computation → Hoare logic, Software and its engineering → Compilers},
  language = {en},
  title = {Correctly Compiling Proofs About Programs Without Proving Compilers Correct},
  volume = {309},
  pages = {33:1-33:20},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2024},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}
}