Proof-carrying Bytecode. - Stephen Gilmore; Matthew Prowse (Bytecode@ETAPS, 2005)