I am a PhD student of computer science with the supervisor, Professor Zhaohui
Department of Computer Science(Mc Crea
Royal Holloway, University of London,
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
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
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.