Embedding Programming Languages in Theorem Provers

The theory of programming languages is one of the core areas of computer sci- ence offering a wealth of models and methods. Yet the complexity of most real programming languages means that a complete formalization of their semantics is only of limited use unless it is supported by mechanical means for reasoning about the formalization. This line of research started in earnest with the seminal paper by Gordon [1] who dened the semantics of a simple while-language in the HOL system and derived Hoare logic from the semantics. Since then, an ever growing number of more and more sophisticated programming languages have been embedded in theorem provers. This talk surveys some of the important developments in this area before concentrating on a specic instance, Bali. Bali (http://isabelle.in.tum.de/Bali/) is an embedding of a subset of Java in Isabelle/HOL. So far, the following aspects have been covered: