Greg Morrisett. Challenges in compiling Coq. In James Cheney, Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016. pages 9, ACM, 2016. [doi]
Abstract is missing.