Accelerating Verified-Compiler Development with a Verified Rewriting Engine

Authors Jason Gross , Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal , Adam Chlipala

Thumbnail PDF


  • Filesize: 1.09 MB
  • 18 pages

Document Identifiers

Author Details

Jason Gross
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA
  • Machine Intelligence Research Institute, Berkeley, CA, USA
Andres Erbsen
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA
Jade Philipoom
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA
  • Google
Miraya Poddar-Agrawal
  • Reed College, Portland, OR, USA
Adam Chlipala
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA

Cite AsGet BibTex

Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala. Accelerating Verified-Compiler Development with a Verified Rewriting Engine. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000× faster while actually featuring simpler compiler-specific proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
  • Software and its engineering → Compilers
  • Software and its engineering → Translator writing systems and compiler generators
  • compiler verification
  • rewriting engines
  • cryptography


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Klaus Aehlig, Florian Haftmann, and Tobias Nipkow. A compiled implementation of normalization by evaluation. In Proc. TPHOLs, 2008. Google Scholar
  2. Nada Amin and Tiark Rompf. LMS-Verify: Abstraction without regret for verified systems programming. In Proc. POPL, 2017. Google Scholar
  3. U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203-211, July 1991. URL:
  4. Mathieu Boespflug. Efficient normalization by evaluation. In Olivier Danvy, editor, Workshop on Normalization by Evaluation, Los Angeles, United States, August 2009. URL:
  5. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In Proc. CPP, 2011. Google Scholar
  6. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In ICFP'08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, Victoria, British Columbia, Canada, September 2008. URL:
  7. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. Elsevier, 1972. Google Scholar
  8. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In IEEE Security & Privacy, San Francisco, CA, USA, May 2019. URL:
  9. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Proc. ICFP, 2002. Google Scholar
  10. Florian Haftmann and Tobias Nipkow. A code generator framework for Isabelle/HOL. In Proc. TPHOLs, 2007. Google Scholar
  11. Jason Hickey and Aleksey Nogin. Formal compiler construction in a logical framework. Higher-Order and Symbolic Computation, 19(2):197-230, 2006. URL:
  12. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179-191. ACM Press, January 2014. URL:
  13. Xavier Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363-446, December 2009. URL:
  14. Gregory Malecha and Jesper Bengtson. Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, chapter Extensible and Efficient Automation Through Reflective Tactics, pages 532-559. Springer Berlin Heidelberg, Berlin, Heidelberg, 2016. URL:
  15. Luc Maranget. Compiling pattern matching to good decision trees. In Proceedings of the 2008 ACM SIGPLAN workshop on ML, pages 35-46. ACM, 2008. URL:
  16. Tiark Rompf and Martin Odersky. Lightweight modular staging: A pragmatic approach to runtime code generation and compiled DSLs. Proceedings of GPCE, 2010. URL:
  17. Zachary Tatlock and Sorin Lerner. Bringing extensibility to verified compilers. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10, pages 111-121, New York, NY, USA, 2010. Association for Computing Machinery. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail