TY - GEN
T1 - Dynamic class initialization semantics
T2 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
AU - Mansky, Susannah
AU - Gunter, Elsa L.
N1 - Publisher Copyright:
© 2019 ACM.
PY - 2019/1/14
Y1 - 2019/1/14
N2 - The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.
AB - The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.
KW - Java
KW - Java Virtual Machine
KW - compilation
KW - dynamic class initialization
KW - interactive theorem proving
KW - operational semantics
KW - type safety
UR - http://www.scopus.com/inward/record.url?scp=85061187475&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85061187475&partnerID=8YFLogxK
U2 - 10.1145/3293880.3294104
DO - 10.1145/3293880.3294104
M3 - Conference contribution
AN - SCOPUS:85061187475
T3 - CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
SP - 209
EP - 221
BT - CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
A2 - Mahboubi, Assia
PB - Association for Computing Machinery, Inc
Y2 - 14 January 2019 through 15 January 2019
ER -