Extracting a formally verified, fully executable compiler from a proof assistant

Stefan Berghofer,Martin Strecker



 
 Abstract

Compilers that have been formally verified in theorem provers are often not directly usable because the formalization language is not a general-purpose programming language or the formalization contains non-executable constructs. This paper takes a comprehensive, even though simplified model of Java, formalized in the Isabelle proof assistant, as starting point and shows how core functions in the translation process (type checking and compilation) are defined and proved correct. From these, Isabelle's program extraction facility generates ML code that can be directly interfaced with other, possibly ``unsafe'' code.
 
 Online Copy

Available as PDF
 
 BibTeX Entry

@InProceedings{berghofer03:_extrac,
  author = 	 {Stefan Berghofer and Martin Strecker},
  title = 	 {Extracting a formally verified, fully executable compiler
                  from a proof assistant},
  booktitle = 	 {Proc. 2nd International Workshop on
                  Compiler Optimization Meets Compiler Verification 
                  (COCV'2003)},
  year =	 2003,
  series =	 {Electronic Notes in Theoretical Computer Science},
  pages=         {33--50}
}


Last modified: Sat Nov 11 20:36:36 CET 2006