Gyesik Lee(ÀÌ°è½Ä)'s Homepage

		Assistant Professor Dept. of Computer & Web Information Engineering, Hankyong National University Address: Second Engineering Bldg (Room 407), 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.

Events

• APLAS 2015 (Local organization chair)
• CPP 2013 (PC member)
• APLAS 2009 (Local organization chair)

Research Interests and Projects

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

• Constructive analysis, type theory, and Coq
  
  "Most mathematicians would find it hard to believe that there could be any serious controversy about the foundations of mathematics, any controversy whose outcome could significantly affect their own mathe- matical activity." -- Errett Bishop in Foundations of Constructive Analysis.
  
  The final goal of this project is to make a contribution to the development of a computer algebra system which can be 100% trusted. We aim at providing libraries such that the interactive theorem prover Coq can act like a computer algebra system. In parallel, we would like to concretize the relationship between Bishop's constructive analysis and Martin-Löf's type theory. This will be a joint project with (at least) two mathematicians in number theory and algebraic geometry.
  
  º» ¿¬±¸ÀÇ ±Ã±ØÀûÀÎ ÁöÇâÁ¡Àº 100% ½Å·ÚÇÒ ¼ö ÀÖ´Â °úÇÐÀû, °øÇÐÀû ¼öÄ¡°è»êÀ» Áö¿øÇÏ´Â ÄÄÇ»ÅÍ ¼ÒÇÁÆ®¿þ¾î ÅøÀ» °³¹ßÇÏ´Â °ÍÀ̸ç, º» ¿¬±¸¸¦ ÅëÇØ ¾ð±ÞµÈ ±Ã±ØÀÇ ÁöÇâÁ¡À» ÇâÇØ ÇÑ ¹ß¦ ÀüÁøÇϱâ À§ÇÑ ÀÌ·ÐÀûÀÌ¸ç ½Ç¿ëÀûÀÎ ±â¹ÝÀ» Á¦½ÃÇÏ´Â °ÍÀ» ÁÖ¿ä ¸ñÇ¥·Î »ï´Â´Ù. À̸¦ À§ÇØ Coq ÀÎÅÍ·¢Æ¼ºê Áõ¸í±â¸¦ ½Ç¿ë¼ºÀ» °®Ãá ÄÄÇ»ÅÍ ´ë¼ö ½Ã½ºÅÛÀ¸·Î °³¹ßÇϴµ¥¿¡ ±â¿©ÇÏ°íÀÚ ÇÑ´Ù. ÀÌ ÇÁ·ÎÁ§Æ®¿¡´Â ÃÖ¼Ò µÎ ¸íÀÇ ¼öÇÐ Àü¹®°¡¿Í ÇÔ²² ÁøÇàµÉ °ÍÀÌ´Ù.

• 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

Journal Articles

• Friedman-Weiermann style independence results beyond Peano arithmetic
  Journal of the Korean Mathematical Society 51(2):383-402, 2014. [Draft].

• Mechanizing Metatheory without Typing Contexts.
  Joint work with Jonghyun Park, Jeongbong Seo, and Sungwoo Park.
  Journal of Automated Reasoning 52(2):215-239, 2014. Visit here.

• 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]

• 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]

Conference Articles

• 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.

• 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]

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

Domestic or Survey Articles

• Formal Metatheory and Recent Developments of Mechanical Developments
  Information 17(7B):3363-3368, 2014. See here