Associate Professor Dept. of Computer Science and Engineering, Hankyong National University Address: 2nd Engineering Bldg (Room 407), Hankyong National University,               327 Jungang-no, Anseong-si, Gyonggi-do. 17579 South Korea Email: gslee [at] hknu [dot] ac [dot] kr Tel.: +82-31-670-5354

Vitae

• Since 04.2015 Associate Professor, Hankyong National University.
• 03.2011 ~ 03.2015 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.

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

• When locally named-becomes becomes nominal
  
  This is a most recent work and submitted to a special issue of JFP on dependently typed programming.
  
  Visit here for more detail.

Drafts

• Proof Pearl: Substitution Revisited, Again
  Gyesik Lee. Visit here

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/Survey Articles

• On Induction Principles in Frege's Grundgesetze and in Systems Thereafter
  Korean Journal of Logic 19(1):83-106, 2016. [Draft]