Pieter H. Hartel, Michael J. Butler, Moshe Levy: The Operational Semantics of a Java Secure Processor. Formal Syntax and Semantics of Java 1999: 313-352