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

Department of Computer Science(Mc

Royal Holloway, University of

Egham,

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

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.