Recent News
UNM receives $1.5 million to support computational workforce development
May 8, 2023
Tapia elected to Computing Research Association Board of Directors
March 3, 2023
UNM computer science students take part in HPC competition
March 3, 2023
Computer science professor, student part of AI panel on March 8
February 24, 2023
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/