CoqJVM : an executable specification of the Java Virtual Machine using dependent types

Atkey, Robert; (2008) CoqJVM : an executable specification of the Java Virtual Machine using dependent types. In: Types for Proofs and Programs (TYPES 2007). Lecture Notes in Computer Science, 4941 . Springer, [Berlin], pp. 18-33. ISBN 9783540681038 (https://doi.org/10.1007/978-3-540-68103-8_2)

[thumbnail of Atkey-LNCS-2008-CoqJVM-an-executable-specification-of-the-Java-Virtual-Machine-using-dependent-types]
Preview
 Text. Filename: Atkey_LNCS_2008_CoqJVM_an_executable_specification_of_the_Java_Virtual_Machine_using_dependent_types.pdf
Accepted Author Manuscript
Download (198kB)| Preview

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.

CORE (COnnecting REpositories)