Toward Type-Preserving Compilation of Coq, at POPL17 SRC (cross-post) 2017-01-03 :: by William J. Bowman