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]
@article{SozeauBFTW20,
title = {Coq Coq correct! verification of type checking and erasure for Coq, in Coq},
author = {Matthieu Sozeau and Simon Boulier and Yannick Forster and Nicolas Tabareau and Théo Winterhalter},
year = {2020},
doi = {10.1145/3371076},
url = {https://doi.org/10.1145/3371076},
researchr = {https://researchr.org/publication/SozeauBFTW20},
cites = {0},
citedby = {0},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
}