Jacek Chrzaszcz. Modules in Coq Are and Will Be Correct. In Stefano Berardi, Mario Coppo, Ferruccio Damiani, editors, Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Volume 3085 of Lecture Notes in Computer Science, pages 130-146, Springer, 2003. [doi]
Abstract is missing.