Verification of Java programs in type theory with dependent record types and coercive subtyping. - Seokhyun Han (2010)