Yves Bertot
Mechanizing the Proof of Correction of a Compiler Using Type Theory
Yves Bertot, Visitor from INRIA, November 17, 1998
Department of Computer Science, Cornell University mtotman
@cs.cornell.edu