University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > An Executable Model of the JVM in Coq

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

An Executable Model of the JVM in Coq

Download to your calendar using vCal

  • UserRobert Atkey, LFCS, Edinburgh
  • ClockFriday 18 May 2007, 14:00-15:00
  • HouseFW11.

If you have a question about this talk, please contact Tom Ridge .

CoqJVM is an executable formalisation of the Java Virtual Machine written in the Coq proof assistant. On one hand it can be extracted from Coq as an O’Caml program and used to execute Java bytecode. On the other hand it can be used to prove the soundness of program logics for bytecode. We intend to use the model to prove the soundness of a program logic and proof checker for proof carrying code. The fact that the model can be executed helps to ensure that the formalisation faithfully models a real Java Virtual Machine.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Small Lecture Theatre, Microsoft Research Room 911, Cavendish Laboratory The George Macaulay Trevelyan Lectures 2012

Other talks

Title to be confirmed Differences between Robin and Neumann eigenvalues The elephant in the room: Machine Learning directly into physical models How Far Can Good Go Without God? The Limits of a Naturalistic Ethic Understanding the Interplay between LLMs' Utilisation of Parametric and Contextual Knowledge Title TBC
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity