Seokhyun Han.

I am a PhD student of computer science with the supervisor, Professor Zhaohui Luo.

Department of Computer Science(Mc Crea Building),
Royal Holloway, University of London,
Egham, Surrey TW20 0EX, U.K.

mail: S.Han @ cs.rhul.ac.uk

  • Mainly, I am researching the use of coercive subtyping and dependent record types in Object-oriented paradigm.
  • Modeling and Verifying Object-oriented programs in Intensional Type theory
  • Functional programming
  • Theoretical apects of Object-oriented programming

MSc in Mathematical logic and the theory of Computation , The university of Manchester .

MSc in Financial Mathematics & Graduate certificate in Mathematical Sciencce, The university of Edinburgh & Heriot-Watt university

===================================================================================
JaCo - The automatic translator for verifying Java programs in Coq.
myJava - A new object-oriented language, which is a subset of Java.
Lexing and BNF syntax of myJava defined by the JavaCC parser.

===================================================================================
Phd Thesis : Verification of Java Programs in Type Theory with Dependent Record Types and Coercive Subtyping, Novemeber, 2010

Verification of Java Programs in Type Theory with Dependent Record Types and Coercive Subtyping, submitted, in the post-proceedings of the Types2009 : Coq codes generated by JaCo MyLibrary.v case1.v

Verification of Java Programs in Coq, accepted[pdf], 2nd Computer Science and Electronic Engineering Conference 2010, The university of Essex: Coq codes generated by JaCo MyLibrary.v case2.v

Verifying Java generic class and inner class in Dependent type theory, To be appeared soon.