Research interests
Verification of embedded systems,
static code analysis
Programming languages, type systems,
category theory
Information security,
verification of cryptographic protocols
|
Papers
On Completeness of Logical Relations for Monadic Types,
in APPSEM'05.
Joint work with S. Lasota and D. Nowak.
Complete Lax Logical Relations
for Cryptographic Lambda-Calculi,
in CSL'2004.
Joint work with J. Goubault-Larrecq, S. Lasota and D. Nowak.
Logical Relations for Dynamic Name Creation,
in CSL'2003.
Joint work with D. Nowak.
|
Education
October 2005, Ph.D.
LSV,
École Normale Supérieure de Cachan, France.
(See the page of my thesis)
September 2002, D.E.A.
(Programmation),
Université Paris 7 - Denis Diderot, France.
June 2002, M.E., Department of Computer Science,
Nanjing University, China.
June 1999, B.S.,
Department of Computer Science,
Nanjing University, China.
|