A formal framework for Java separate compilation

DOI10.1007/3-540-47993-7_26MaRDI QIDQ3046765zbMATH OpenFDO

Authors Davide Ancona, Giovanni Lagorio, Elena Zucca

Publication date 12 August 2004

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/2374/23740609.htm

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computing methodologies and applications (68U99)

Recommendations

• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Formal verification of a Java compiler in Isabelle
• Java and the Java memory model -- a unified, machine-checked formalisation
• A type system for the Java bytecode language and verifier
• Verified bytecode verification and type-certifying compilation

Cited in

(10)

• Formalization and analysis of class loading in Java
• Formalising Java RMI with explicit code mobility
• ADiJaC -- Automatic Differentiation of Java Classfiles
• Principal typings for Java-like languages
• Type Inference by Coinductive Logic Programming
• scientific article; zbMATH DE number 1497837 (Why is no real title available?)
• Formal techniques for Java programs
• Towards a smart compilation manager for Java (extended abstract)
• A flexible model for dynamic linking in Java and C\#
• A core calculus for correlation in orchestration languages

This page was built for publication: A formal framework for Java separate compilation

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