Recent News
At Hand and Machine Lab event, art was a two-way interactive experience
June 2, 2022
Computer science changed UNM grad’s tune on a career
May 18, 2022
Computer science graduate student to compete in climbing world championships in May
April 26, 2022
Computer science graduate student receives Griffith Fellowship
April 19, 2022
News Archives
A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler
December 1, 2005
- Date: Thursday, December 1st, 2005
- Time: 11:00-12:15pm.
- Place: Woodward 149
Prof. Dr. Tobias Nipkow Department of Informatik Technical University of Munich Germany
We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between realism of the language and tractability and clarity of the formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialisation analysis; a type safety proof of the small step semantics; a virtual machine (JVM), its operational semantics and its type system; a type safety proof for the JVM; a bytecode verifier, i.e. data flow analyser for the JVM; a correctness proof of the bytecode verifier w.r.t. the type system; a compiler and a proof that it preserves semantics and well-typedness.
The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL jointly with Gerwin Klein.
The talk will give a very high-level overview of these formalizations. Full paper available at www.in.tum.de/~nipkow/pubs/Jinja/