Welcome to Gyesik Lee's homepage

I am a postdoc at ROSAEC center (Research On Software Analysis for Error-free Computing) of Seoul National University.

I got my Ph.D. at Institute for Mathematical Logic and Foundation, Univ. of Münster, Germany
Previous positions: postdoc at LogiCal (now called TypiCal) at l'INRIA-Futurs in France and at RCIS of AIST in Japan.

Main research interests are mathematical logic (type theory and proof theory) and formal methods.
You may have a look at my research papers.

Currently, I am working on the following subjects.

• Constructive proof of completeness of classical or intuitionistic logic systems w.r.t. Kripke semantics.
  Together with Hugo Herbelin and Danko Ilik.

• Formalization of Normalization by Evaluation based on the first-order logic and Kripke semantics.
  Together with Hugo Herbelin.

• Planning to work on formalization of F_< in connection with generic programming.
  Together with Bruno Oliveira and Chung-Kil Hur.

• Formal methods in cryptology, especially interested in automatic verification of security protocols.

• The other is related to type theoy, logic, and theorem proving on top of Coq.

If you are interested you can have a look at my CV (updated on Oct. 22, 2009).

---

To contact me: gslee [at]  ropas.snu.ac.kr

ROSAEC center, Room 215 Bldg 138, Seoul National University, 599 Gwanak-ro Gwanak-gu, Seoul 151-742, KOREA
Tel: +82-2-880-1532, Fax: +82-2-882-7234

---

Last modified: Oct. 22, 2009