Precision in practice: A type-preserving Java compiler

DOI10.1007/3-540-36579-6_8MaRDI QIDQ4417787zbMATH OpenFDO

Authors Christopher League, Zhong Shao, Valery Trifonov

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2622/26220106.htm

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Computing methodologies and applications (68U99)

Recommendations

• Verified bytecode verification and type-certifying compilation
• Formal verification of a Java compiler in Isabelle
• A type system for the Java bytecode language and verifier
• scientific article; zbMATH DE number 1231622
• Towards proving type safety of .NET CIL

Cited in

(6)

• Verified bytecode verification and type-certifying compilation
• A representation of \(F_{\omega}\) in LF
• Type safety in the JVM: some problems in Java 2 SDK 1.2 and proposed solutions
• scientific article; zbMATH DE number 2165694 (Why is no real title available?)
• scientific article; zbMATH DE number 5593262 (Why is no real title available?)
• Security types preserving compilation

This page was built for publication: Precision in practice: A type-preserving Java compiler

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