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

Java\(\mu\)Java\(\mu\)JVM

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

(11)

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

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle

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)