Java: Embedding a programming language in a theorem prover

MaRDI QIDQ2752051zbMATH OpenFDO

Authors Tobias Nipkow, David von Oheimb, Cornelia Pusch

Publication date 23 October 2002

zbMATH Keywords

\(\mu\)Java\(\mu\)JVMJava

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• scientific article; zbMATH DE number 2090288
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 1980940
• Hoare logic for Java in Isabelle/HOL
• scientific article; zbMATH DE number 1701360

Cited in

(14)

• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Verified bytecode verifiers.
• Verified bytecode verification and type-certifying compilation
• Turning Inductive into Equational Specifications
• Ivor, a Proof Engine
• Verified lightweight bytecode verification
• An embedding of Ruby in Isabelle
• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• scientific article; zbMATH DE number 5593262 (Why is no real title available?)
• Jinja: towards a comprehensive formal semantics for a Java-like language
• Theorem Proving in Higher Order Logics
• The HOL-CSP Refinement Toolkit
• HOL-CSP Version 2.0
• A Sound Type System for Physical Quantities, Units, and Measurements

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: \(\mu\)Java: Embedding a programming language in a theorem prover

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