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

DOI10.1007/978-3-540-68103-8_2zbMATH Open1138.68344OpenAlexW1554855925MaRDI QIDQ3499747FDOQ3499747

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

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

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Title not available (Why is that?)
• Towards a mechanized metatheory of standard ML
• Executable JVM model for analytical reasoning: A study
• Formal certification of a compiler back-end or
• The Java memory model
• Title not available (Why is that?)
• Formalising Java’s Data Race Free Guarantee
• Title not available (Why is that?)

Cited In (3)

• Animating the Formalised Semantics of a Java-Like Language
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• CoqJVM

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)