CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
Source: University of Edinburgh
The authors 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. They describe the structure of the formalisation and the way in which they have used dependent types.