Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman. Œuf: minimizing the Coq extraction TCB. In June Andronick, Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. pages 172-185, ACM, 2018. [doi]
Abstract is missing.