Gyesik Lee's Homepage

		Assistant Professor Dept. of Computer & Web Information Engineering, Hankyong National University Address: I-dong 401, Hankyong National University, 327 Jungang-no, Anseong-si, Kyonggi-do. 456-749 KOREA Email: gslee [at] hknu [dot] ac [dot] kr Tel.: +82-31-670-5354

Vitae

• Since 03.2011 Assistant Professor, Hankyong National University.
• 04.2009 ~ 02.2011 Postdoc, ROSAEC center (Research On Software Analysis for Error-free Computing), Seoul National University.
• 12.2007 ~ 03.2009 Postdoc, RCIS, AIST, Japan.
• 12.2005 ~ 06.2007 Postdoc, LogiCal (now called TypiCal), INRIA, France.
• 04.2005 Ph.D., Institute for Mathematical Logic, Univ. of Münster, Germany.
• 12.1996 Master, Institute for Mathematical Logic, Univ. of Münster, Germany.
• 02.1992 B.S., Dept. of Mathematics, Seoul National University.

Current Events

Research Interests

My research interests are mainly focused on logic and formal methods.

Projects

• Reverse Mathematics in Coq
  
  One of the goals of our project is to reformulate the languages of reverse mathematics in a way that the new languages become both finer (thanks to analysis in terms of polarization) and more useful in practice (thanks to the use of concepts from type theorie such as inductive types, dependent products). The success of Coq in the history of the formalization of mathematics shows that the goal is very natural. Another goal is to integrate the new languages into Coq so that it can serve the research on reverse mathematics. We will then be able to provide a concrete framework which any logician or mathematician interested in formalizing the results of reverse mathematics can use.
  
  Visit here for more detail.

• Formalizing Logical Metatheory
  
  We propose an approach to dealing with binding issues when formalizing the metatheory of a logical system with variables such as first-order predicate logic. In our approach, the syntax is represented with locally traced names. The style is similar to Pollack-McKinna's locally-named approach, in which two sorts of named variables are used. The main difference is that (locally bound) variables occurring in an expression are controlled by the type of that expression. This approach has been adopted to formalize in Coq a Kripke-based semantical cut-elimination of intuitionistic first-order predicate logic.
  
  Visit here for more detail.

Publications

• Friedman-Weiermann style independence results beyond Peano arithmetic
  Journal of the Korean Mathematical Society. To appear. [Draft].

• Mechanizing Metatheory without Typing Contexts.
  Joint work with Jonghyun Park, Jeongbong Seo, and Sungwoo Park. Journal of Automated Reasoning. April, 2013. Visit here.

• GMeta: A Generic Formal Metatheory Framework for First-Order Representations.
  Joint work with Bruno C.d.S. Oliveira, Sungkeun Cho, Kwangkeun Yi.
  The 22nd European Symposium on Programmin, ESOP 2012, LNCS 7212: 436-455. Visit GMeta homepage.

• Proof-irrelevant model of CC with predicative induction and judgmental equality.
  Joint work with Benjamin Werner.
  Logical Methods in Computer Science 7 (4:5), 2011. [Draft].

• Sharp Thresholds for hypergraph regressive Ramsey numbers.
  Joint work with Lorenzo Carlucci and Andreas Weiermann.
  Journal of Combinatorial Theory, Series A 118(2): 558-585, 2011. [Draft]

• Kripke Models for Classical Logic.
  Joint work with Danko Ilik and Hugo Herbelin.
  Special Issue on "Classical Logic and Computation" (CL&C) '08, Annals of Pure and Applied Logic 161 (11), 2010. [Draft]

• Formally Verifiable Features in Embedded Vehicular Security Systems.
  Joint work with Hisashi Oguma, Akira Yoshioka, Rie Shigetomi, Akira Otsuka and Hideki Imai.
  First IEEE Vehicular Networking Conference, VNC 2009, Tokyo. IEEE Xplore database. [Draft]

• Relationship between Kanamori-McAloon principle and Paris-Harrington theorem.
  Computability in Europe, CiE 2009, LNCS 5635: 310-323. [Draft]

• Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus
  Joint work with Hugo Herbelin.
  Logic, Language, Information and Computation, 16th International Workshop, Wollic 2009, LNAI 5514: 209-217. [Draft]

• Sharp threshold for the phase transition between primitive recursive and Ackermannian Ramsey numbers.
  Joint work with Menachem Kojman, Eran Omri and Andreas Weiermann.
  Journal of Combinatorial Theory, Series A. 115(6):1036-1055, 2008. [Draft]

• A comparison of well-known ordinal notation systems for &epsilon _0.
  Annals of Pure and Applied Logic 147 (1-2) (2007): 48-70. [Draft]

• Binary trees and (maximal) order types.
  Computation and Logic in the Real World, CiE 2007, LNCS 4497:465-473. [Draft] [Extended draft]

Ph.D. thesis

• Phase Transitions in Axiomatic Thought.
  Ph.D. thesis, Univ. of Münster, Germany, viii, 110~p, April, 2005.
  ( Review by Prof. Andrea Cantini in Zentralblatt)

Master thesis

• Repräsentierbarkeit innerhalb des Lambda-Würfels (written in German)
  (Title in English: Representability within the Lambda cube)
  Master thesis, Univ. of Münster, Germany, iv, 129~p, December 1996.
  Extended abstract in English here.