Welcome to Gyesik Lee


		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

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.

Exact Real Arithmetic

"We propagate Exact Real Arithmetic (ERA) as a both convenient and practically efficient framework for rigorous numerical algorithms." -- Norbert Müller and Martin Ziegler in From Calculus to Algorithms without Errors

We'd like to implement ERC as imperative programming languages and prove the soundness of the system using a proof assistant or a theorem prover. Visit here for more detail.

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.

Principal Investigator in Development of Algorithms for Exact Real Arithmetic from Theory to Practice funding by NRF #2017R1D1A1B05031658

Joint Researcher in Computing with Infinite Data, EU H2020 MSCA IRSES #731143 cofunding by NRF #2016K1A3A7A03950702
(Principal Investigator: Martin Ziegler)

Corresponding Partner of CORCON-Correctness by Construction, Seventh Framework Programme of the European Union Marie Curie Actions-People IRSES #612638

Formalizing the meta-theory of first-order predicate logic
Joint work with Hugo Herbelin and SunYoung Kim.
Journal of the Korean Mathematical Society 54(5):1521-1536, 2017. [Draft].

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]

On Formal Verification in Imperative Multivalued Programming over Continuous Data Types
Joint work with Norbert Müller, Eike Neumann, Sewon Park, Norbert Preining, Martin Ziegler
Submitted to MACIS 2017.

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]

Frege's influence on the modern practice of doing mathematics
Korean Journal of Logic 20(1):97-112, 2017. [Draft]

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

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

How to Formally Model Features of Network Security Protocols
International Journal of Security and Its Applications 8(1):423-432, 2014. [Draft]

콕 증명보조기에서 한 가지 변수 이름을 사용하는 노미널 방식 활용하기
Joint work with Hyeon-Suk Na.
정보과학회논문지: 소프트웨어 및 응용 40(11), 2013. [Draft]

A Note on Kruskal's Theorem
Joint work with Hyeon-Suk Na.
Korean Journal of Logic 15(3):307-321, 2012 [Draft]

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)

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.

Last modification: October 2017