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 |