Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
(pdf)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), New Orleans, USA