Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one-pass verification of well-typedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness. Copyright.
展开▼
