CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types

Publication Information

Robert Atkey. CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers, volume 4941 of Lecture Notes in Computer Science, 18-32. Springer, 2007.
DOI: 10.1007/978-3-540-68103-8_2

Abstract

We describe an executable specification of the Java Virtual Machine (JVM) within the Coq proof assistant. The principal features of the development are that it is executable, meaning that it can be tested against a real JVM to gain confidence in the correctness of the specification; and that it has been written with heavy use of dependent types, this is both to structure the model in a useful way, and to constrain the model to prevent spurious partiality. We describe the structure of the formalisation and the way in which we have used dependent types.