Java and the Java Virtual Machine: Definition, Verification, Validation

By Robert F. Stärk, J. Schmid, E. Börger. 2001

408 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/a3b1e5da60d4d1ac6eb58e465891d3402efebb62

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Gerwin Klein
2. Tobias Nipkow
3. Stanislas Nanchen
4. Robert F. Stärk
5. Xavier Leroy
6. The mathlib Community

Citations in the corpus

• A machine-checked model for a Java-like language, virtual machine, and compiler (2006, methodology): “For that purpose we follow Stärk et al. [2001] and define a “type compiler” that compiles an expression into type annotations (a method type) for the instruction list that compE 2 produces: compT :: ty list ⇒ nat set option ⇒ ty list ⇒ expr1 ⇒ tyi ′ list As in §4.”
• A Logic for Abstract State Machines (2001, methodology): “for compiler correctness proofs from Prolog to the WAM [Schmitt 1994] or from Java to the JVM [Stärk et al. 2001].”