Abstract:
|
Bicolano is a formal definition of the Java Bytecode Semantics in Coq. It will be used as a reference semantics in the Mobius project. In a first part of the talk I will present the global structure of the development. In a second part I will introduce an intermediate bigstep semantics with a correspondance proof. |