Subject: Investigating the usefulness of the Java Byte Code Verifier specified in Natural Semantics Jour: 10/03/98 (Mardi 10 mars 98) http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ ___ / _ _ / __ __ /_ _ / / | _ __ _ / / \ / \ ___ / / | / /_ / __| / ___ /___/ __| / | __| |___ |_/ |_/ |____ / / __/ |_ |_/ |_ / |_/ / |_/ / / I N R I A - Rocquencourt, Salle de confe'rence du batiment 11 Mardi 10 mars, 14h ------------------- Eva Rose ------------------- LIP ENS Lyon - equipe PLUME ============================================================ A tour of a Java subset operational-semantics and its proofs ============================================================ We present a static and dynamic semantics of a subset of Java (JavaOb), its translation to the Java Virtual Machine (JVM), and a static and dynamic semantics for the restricted machine (JVMOb). All specified by means of operational semantics, specifically Kahn's "natural semantics" (1987). We give some examples of proofs in this formalism, and invite the audience to participate in a discussion of HOW to formalize this in Coq (and why). Ce travail a été réalisé a DIKU, Danemark sous la direction de Mads Tofte