KnowledgeBase » 
SEMINAR
» ID = 500
Mechanizing the Proof of Correction of a Compiler Using Type Theory
by Yves Bertot
1998-1999
Yves Bertot, Visitor from INRIA
As a case study, we have concentrated on the proof that a compiler respects the meaning of the programs it compiles: the compiled program (a program in some assembly language) will always perform exactly the same computations as the source program. This proof has been completely formalized using the Inductive Calculus of Constructions, a variant of type theory that makes it easy to describe the semantics of the two programming languages and the behavior of the compiler.
The main contributions of this work are three theorems that make it easier to turn around the difficulties of reasoning on unstructured programs where control is expressed with conditional and unconditional goto statements.
