이계식 교수 (Gyesik Lee, Professor)

컴퓨터응용수학부 소프트웨어융합 전공 한경국립대학교 (경기도 안성시 중앙로 327) Email: gslee  @  hknu.ac.kr

×

강의(Courses)

• 참고: 코딩알지 강의노트 모음 웹사이트

연구관심분야(Research Interests)

• 데이터 분석(Data Analysis)
• 프로그래밍 언어론(Programming Languages)
• 정밀 실수연산(Exact Real Computation)
• 정형검증(Mechanization and Verification of Proofs)
• 수리논리와 수학기초론(Mathematical Logic and Foundation)

최근 연구(Current Research)

• 데이터 분석
  • 4대강 보 수질 데이터 분석

    참고 논문: Algae Development in Rivers with Artificially Constructed Weirs: The Dominant Influence of Discharge Over Temperature (Journal Of Environmental Management)

  • 암모니아 배출 데이터 분석

    참고 논문: Comparison of ammonia volatilization in paddy and field soils fertilized with urea and ammonium sulfate during rice, potato, and Chinese cabbage cultivation (Atmospheric Pollution Research)

• 정밀 실수 연산(Exact Real Arithmetic, ERA) 이론 정립

  참고 논문: Semantics, Specification Logic, and Hoare Logic of Exact Real Computation (Logical Methods in Computer Science)

프로젝트(Projects)

참여 과제(Current Projects)

• 감축수단 이행을 위한 벼재배 메탄 보정계수 개발 및 현장 적용 (주관: 경상국립대)

이전 참여 과제(Previous Projects)

• 엄밀한 실수 연산을 위한 알고리즘 개발: 이론에서 응용까지 (Development of Algorithms for Exact Real Arithmetic from Theory to Practice), 한국연구재단(NRF)
• Computing with Infinite Data, EU H2020 MSCA IRSES cofunded by NRF (Principal Investigator: Martin Ziegler)
• Corresponding Partner of CORCON-Correctness by Construction Seventh Framework Programme of the European Union Marie Curie Actions-People IRSES #612638
• 수학자들이 사용하기 쉬운 증명보조기 소프트웨어 개발 (Reverse Mathematics in Coq), STAR Project, 한국-프랑스 협력기반조성 사업 지원과제, 2012. 공동연구(joint work with): Hugo Herbelin, INRIA, France. Project homepage: Reverse Mathmatics in Coq
• 형식적 수리논리 연구를 지원하는 증명보조기(proof assistant) 개발 연구 (Research on developing a proof assistant for formal mathematical logic), 한국연구재단(NRF)

약력(Vitae)

• 조교수/부교수(03.2011-03.2020), Hankyong National University.
• 연구원(04.2009-02.2011), ROSAEC Center (Research On Software Analysis for Error-free Computing), Seoul National University.
• 연구원(12.2007-03.2009), RCIS, AIST, Japan.
• 박사후연구원(12.2005-06.2007), LogiCal (now called TypiCal), INRIA, France.
• Ph.D.(04.2005), Institute for Mathematical Logic, Univ. of Münster, Germany.
• 석사(12.1996), Institute for Mathematical Logic, Univ. of Münster, Germany.
• 이학사(수학전공)(02.1992), Seoul National University.

논문과 저역서(Publications)

저역서

• 기초 수학 - 새롭게 다시 읽다. John Stillwell(저자), 김영주, 이계식, 최인송 (역자), 북스힐, 2022. (2023 세종도서 학술부문 추천도서)
• Proceedings of the 14th and 15th Asian Logic Conferences. Byunghan Kim, Jörg Brendle, Gyesik Lee, Fenrong Liu, R Ramanujam, Shashi M Srivastava, Akito Tsuboi, and Liang Yu(Editors), World Scientific, 2019.

국제저널(Journal Articles)

• Semantics, Specification Logic, and Hoare Logic of Exact Real Computation. Joint work with Sewon Park, Franz Brauße, Pieter Collins, SunYoung Kim, Michal Konečný, Norbert Müller, Eike Neumann, Norbert Preining, Martin Ziegler. Logical Methods in Computer Science 20(2), pp. 17:1-17:55, 2024.
• Algae Development in Rivers with Artificially Constructed Weirs: Dominant Influence of Discharge Over Temperature. Joint work with Hyunju Kim, Chang-Gu Lee, Seong-Jik Park. Journal of Environmental Management 355:120551, 2024.
• Comparison of ammonia volatilization in paddy and field soils fertilized with urea and ammonium sulfate during rice, potato, and Chinese cabbage cultivation. Joint work with Yeon-Jin Lee, Eun-Chae Im, Sung-Chang Hong, Chang-Gu Lee, Seong-Jik Park. Atmospheric Pollution Research 15(4), 2024.
• Refinement of homogeneity and Ramsey numbers. Joint work with Hwajeong Kim. Communications of the Korean Mathematical Society 33(3):1001-1011, 2018. [Draft].
• 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]

국제학회지(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)

• PaperCleaner, an Automatic Restoration Program of Korean Documents Based on GAN Algorithm. 공동저자: 김민규, 임형택. Journal of Knowledge Information and Systems 17(6):1331-1339, 2022. [Draft]
• A Machine Learning System for Crosswalk Detection(횡단보도 탐지 머신러닝 시스템). 공동저자: 박주석. Journal of Knowledge Information and Systems 16(1):9-19, 2021. [Draft]
• A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence(호어 논리와 커리-하워드 대응관계 사이의 연관성 분석). 공동저자: 김화정. Journal of Knowledge Information and Systems 15(2):189-193, 2020. [Draft]
• 암호화 보안 프로토콜의 정형명세. Journal of Knowledge Information and Systems 14(6):711-718, 2019. [Draft]
• Locally-named versus Nominal. Joint work with Hwajeong Kim Journal of Engineering and Applied Sciences 13(19):7878-7883, 2018. [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]
• 콕 증명보조기에서 한 가지 변수 이름을 사용하는 노미널 방식 활용하기. 공동저자: 나현숙. 정보과학회논문지: 소프트웨어 및 응용 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]
• 프로그래밍 언어 메타이론의 정형화 및 변수 묶기. 정보과학회논문지: 소프트웨어 및 응용 35(12), 2008. [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.