취업 및 행사 정보

공지 시작  
공지 종료  
Date:August 27, 2014
Time: 4:30PM-5:30PM
Location: NIMS, CAMP seminar room (국가수리과학연구소 수학원리응용센터 세미나실)

[Title]

Mechanization of Proof: From 4-Color Theorem to Compiler Verification.

[Abstract]

I will give a broad introduction to how to mechanize mathematics (or proof), which will be mainly about the proof assistant Coq.Mechanizing mathematics consists of (i) defining a set theory, (2) developing a tool that allows writing definitions and proofs in the set theory, and (3) developing an independent proof checker that checks whether a given proof is correct (ie, whether it is a valid combination of axioms and inference rules of the set theory).  Such a system is called proof assistant and Coq is one of the most popular ones.

In the first half of the talk, I will introduce applications of proof assistant, ranging from mechanized proof of 4-color theorem to verification of an operating system. Also, I will talk about a project that I lead, which is to provide, using Coq, a formally guaranteed way to completely detect all bugs from compilation results of the mainstream C compiler LLVM.

In the second half, I will discuss the set theory used in Coq, called Calculus of (Inductive and Coinductive) Construction. It will give a very interesting view on set theory. For instance, in calculus of construction, the three apparently different notions coincide: (i) sets and elements, (ii) propositions and proofs, and (iii) types and programs.

If time permits, I will also briefly discuss how Von Neumann Universes are handled in Coq and how Coq is used in homotopy type theory, led by Fields medalist Vladimir Voevodsky.

[Speaker]

Chung-Kil Hur (허충길)

[Short-Bio]

Chung-Kil Hur is an assistant professor in Department of Computer Science and Engineering at Seoul National University.  Previously he worked as a postdoctoral researcher at Microsoft Research Cambridge, Max Planck Institute for Software Systems (MPI-SWS) and Laboratoire PPS. He obtained a Ph.D. from University of Cambridge and a B.Sc. in Mathematics and in Computer Science from KAIST. He also received a bronze medal in the 35th International Mathematical Olympiad (IMO) in 1994.  His research interests are in software verification, interactive theorem proving, probabilistic programming and Beyesian inference.
번호 제목 글쓴이 날짜 조회 수
공지 [넛지헬스케어_캐시워크] 데이터분석 담당 산업기능요원 모집 과사무실 2025.07.03 22
공지 KAIST 수리과학과 4단계 BK21 연구교수 모집 공고 과사무실 2025.06.16 1836
708 [현대오토에버]2018년 상반기 신입/인턴사원 공개채용 file 과사무실 2018.03.08 2096
707 [LG이노텍] 2018 상반기 대졸신입 채용 및 교내 채용상담 file 과사무실 2018.03.07 2901
706 [하이트진로] 2018 대졸 공채 및 공장견학설명회 과사무실 2018.03.07 4739
705 [한화케미칼] '18년 상반기 한화케미칼 신입사원 모집 file 과사무실 2018.03.05 2480
704 [LG CNS] IT Leadership Academy (2018 상반기 신입사원 채용) file 과사무실 2018.03.05 2205
703 [삼성SDI] 2018년 상반기 삼성SDI 공채/인턴 채용 file 과사무실 2018.03.05 2330
702 (국가보안기술연구소) 2018년도 1차 정규직(연구직, 기술직) 채용 공고(~3/7) file 과사무실 2018.02.22 7984
701 [삼성디스플레이] 한국과학기술원(수리과학과) 캠퍼스 리크루팅 file 과사무실 2018.02.22 2448
700 [월드퀀트] 글로벌 퀀트 회사 월드퀀트의 International Quant Championship 과사무실 2018.02.20 2633
699 (2차설명회)[SK하이닉스] 2018_상반기_SK하이닉스 TALK+ 수시 채용설명회 과사무실 2018.02.06 2448
698 [LG이노텍] CTO 광학기술 신입(석사이상) 사원 모집(~2/9) 과사무실 2018.02.02 2101
697 Streami Inc. is a blockchain startup working with leading financial service providers in Asia with the mission of bringing open, affordable, and efficient financial services. 과사무실 2018.02.01 4520
696 (1차설명회)[SK하이닉스] 2018_상반기_SK하이닉스 TALK+ 수시 채용설명회 모집 file 과사무실 2018.02.01 2454
695 [삼성디스플레이] 한국과학기술원(수리과학과) 대학생 초청행사 참가자 추천 공문 file 과사무실 2018.01.31 11848
694 삼성SDS 채용상담 및 SDS 잠실 Campus Tour 안내 과사무실 2018.01.26 2457
693 [LG CNS] 18년 동계인턴십 모집 file 과사무실 2018.01.11 2445
692 [LG CNS] 2018 동계 Smart IT 인턴십 모집(~18.01.14) 과사무실 2018.01.10 2275
691 [LG CNS] 2018 국내외 석박사 채용 file 과사무실 2017.12.22 2444
690 [LG CNS] 2018 동계 Smart IT 인턴십 모집 file 과사무실 2017.12.22 3489
689 [동화그룹] 2017 동화그룹 대졸신입 공개채용(~12/26) 과사무실 2017.12.18 2093
688 수리과학과 BK21플러스 사업단 연수연구원 초빙 공고(12월31일 마감) file 과사무실 2017.12.11 2222
687 [Event] KAIST-KIAS JOINT WORKSHOP IN THEORETICAL SCIENCES file 과사무실 2017.12.08 2081
686 2018년도 1학기 숭실대학교 수학과 연구중점교원 특별초빙 과사무실 2017.12.04 4925
685 [현대엠엔소프트] 2018년 채용연계형 인턴사원 모집[12.6~12.11] 과사무실 2017.12.04 2383
684 [LG전자]한국영업본부 채용연계형 인턴사원 5기 모집 과사무실 2017.12.04 3244
683 [LG전자]한국영업본부 채용연계형 인턴사원 5기 모집 과사무실 2017.12.04 1967
682 [한샘] '18년 상반기 신입SC 공개 채용 과사무실 2017.12.01 2072
681 미래에셋자산운용 금융공학/포트폴리오운용본부 인턴 채용 file 과사무실 2017.11.28 3107
680 [하포리서치코리아] 리서치 인턴 구인 과사무실 2017.11.23 3133
679 [삼성SDS] 석사·박사 채용 상담 file 과사무실 2017.11.17 8382