CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
From MaRDI portal
Publication:3499747
DOI10.1007/978-3-540-68103-8_2zbMath1138.68344OpenAlexW1554855925MaRDI QIDQ3499747
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ CoqJVM
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Executable JVM model for analytical reasoning: A study
- Towards a mechanized metatheory of standard ML
- Formalising Java’s Data Race Free Guarantee
- The Java memory model
- Formal certification of a compiler back-end or
This page was built for publication: CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
