Binary Trees and (Maximal) Order Types. - Gyesik Lee (CiE, 2007)

A comparison of well-known ordinal notation systems for epsilon0. - Gyesik Lee (Ann. Pure Appl. Log., 2007)

Sharp thresholds for the phase transition between primitive recursive and Ackermannian Ramsey numbers. - Menachem Kojman; Gyesik Lee; Eran Omri; Andreas Weiermann (J. Comb. Theory A, 2008)

Relationship between Kanamori-McAloon Principle and Paris-Harrington Theorem. - Gyesik Lee (CiE, 2009)

Formally verifiable features in embedded vehicular security systems. - Gyesik Lee; Hisashi Oguma; Akira Yoshioka; Rie Shigetomi; Akira Otsuka; Hideki Imai (VNC, 2009)

Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. - Hugo Herbelin; Gyesik Lee (WoLLIC, 2009)

Kripke models for classical logic. - Danko Ilik; Gyesik Lee; Hugo Herbelin (Ann. Pure Appl. Log., 2010)

Proof-irrelevant model of CC with predicative induction and judgmental equality - Gyesik Lee; Benjamin Werner (Log. Methods Comput. Sci., 2011)

Sharp thresholds for hypergraph regressive Ramsey numbers. - Lorenzo Carlucci; Gyesik Lee; Andreas Weiermann (J. Comb. Theory A, 2011)

GMeta: A Generic Formal Metatheory Framework for First-Order Representations. - Gyesik Lee; Bruno C. d. S. Oliveira; Sungkeun Cho; Kwangkeun Yi (ESOP, 2012)

Mechanizing Metatheory Without Typing Contexts. - Jonghyun Park; Jeongbong Seo; Sungwoo Park; Gyesik Lee (J. Autom. Reason., 2014)

Semantics, Specification Logic, and Hoare Logic of Exact Real Computation. - Sewon Park 001; Franz Brauße; Pieter Collins; SunYoung Kim; Michal Konecný; Gyesik Lee; Norbert Th. Müller; Eike Neumann; Norbert Preining; Martin Ziegler 001 (Log. Methods Comput. Sci., 2024)