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

DOI10.1007/978-3-540-68103-8_2MaRDI QIDQ3499747zbMATH OpenOpenAlexFDO

Authors Robert Atkey

Publication date 3 June 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://strathprints.strath.ac.uk/74424/1/Atkey_LNCS_2008_CoqJVM_an_executable_specification_of_the_Java_Virtual_Machine_using_dependent_types.pdf

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• scientific article; zbMATH DE number 1692947
• scientific article; zbMATH DE number 1927413
• scientific article; zbMATH DE number 2090288
• scientific article; zbMATH DE number 2086505
• Preservation of Proof Obligations from Java to the Java Virtual Machine

Cites work

• scientific article; zbMATH DE number 1650458 (Why is no real title available?)
• scientific article; zbMATH DE number 1692947 (Why is no real title available?)
• scientific article; zbMATH DE number 1330435 (Why is no real title available?)
• Executable JVM model for analytical reasoning: A study
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formalising Java’s Data Race Free Guarantee
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The Java memory model
• Towards a mechanized metatheory of Standard ML

Cited in

(3)

• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• CoqJVM
• Animating the formalised semantics of a Java-like language

Describes a project that uses

Uses Software

• Coq

This page was built for publication: CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3499747)