Programming a JVM using dependent types

Robert Atkey, University of Edinburgh

I have been constructing an executable specification of the Java Virtual Machine in the interactive theorem prover Coq. The ultimate goal of this work is to have a formal specification of the JVM that can be used to prove the soundness of program logics reasoning about Java bytecode programs. The model is designed to be executable, so that it can be tested against the real JVM in order to gain confidence that I am modelling the correct thing. I have made heavy use of dependent types to structure the program. In this talk I will give an overview of the development and describe my experiences programming with dependent types.