Verified bytecode verification and type-certifying compilation
scientific article; zbMATH DE number 2107869