BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:An Executable Model of the JVM in Coq - Robert Atkey\, LFCS\, Edin
 burgh
DTSTART:20070518T130000Z
DTEND:20070518T140000Z
UID:TALK7347@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:CoqJVM is an executable formalisation of the Java Virtual Mach
 ine\nwritten in the Coq proof assistant. On one hand it can be extracted f
 rom\nCoq as an O'Caml program and used to execute Java bytecode. On the ot
 her\nhand it can be used to prove the soundness of program logics for\nbyt
 ecode. We intend to use the model to prove the soundness of a program\nlog
 ic and proof checker for proof carrying code. The fact that the model\ncan
  be executed helps to ensure that the formalisation faithfully models\na r
 eal Java Virtual Machine.
LOCATION:FW11
END:VEVENT
END:VCALENDAR