Abstract

This talk presents the formalization and interactive proof of type safety of a large subset (called Bali) of the sequential part of the programming language Java carried out with the help of the theorem prover Isabelle/HOL. After an introduction to the basics of Java and Isabelle/HOL, I will sketch the formalization of Bali (its abstract syntax, typed system and operational semantics) and discuss the formal proof of type safety. This should demonstrate that machine-checking the design of non-trivial programming languages has become more than just a theoretical possibility.

This work is part of a larger project which aims to formalize not just the source language Java but also the Java Virtual Machine, the byte code verifier and other relevant parts of the execution environment.