Animating the Formalised Semantics of a Java-Like Language
From MaRDI portal
Publication:3088008
DOI10.1007/978-3-642-22863-6_17zbMath1342.68294OpenAlexW2106047869MaRDI QIDQ3088008
Lukas Bulwahn, Andreas Lochbihler
Publication date: 17 August 2011
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_17
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ From LCF to Isabelle/HOL
Uses Software
Cites Work
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- A formally verified compiler back-end
- Turning Inductive into Equational Specifications
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Certification of Termination Proofs Using CeTA
- CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
- Extraction in Coq: An Overview
- Imperative Functional Programming with Isabelle/HOL
- Verifying a Compiler for Java Threads
- Code Generation via Higher-Order Rewrite Systems
- Algebraic Methodology and Software Technology
- The Isabelle Collections Framework
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
This page was built for publication: Animating the Formalised Semantics of a Java-Like Language
