Coq Coq correct! verification of type checking and erasure for Coq, in Coq

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, 4(POPL), 2020. [doi]

Abstract

Abstract is missing.