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

Research output: Chapter in Book/Report/Conference proceedingChapter

8 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationTypes for Proofs and Programs (TYPES 2007)
Subtitle of host publicationLecture Notes in Computer Science
Place of Publication[Berlin]
PublisherSpringer
Pages18-33
Number of pages16
Volume4941
ISBN (Print)9783540681038
DOIs
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume4941

Keywords

  • Java Virtual Machine
  • JVM
  • Coq proof assistant

Fingerprint Dive into the research topics of 'CoqJVM: an executable specification of the Java Virtual Machine using dependent types'. Together they form a unique fingerprint.

Cite this