# NIMS세미나 (8월 27일): 허충길 교수, Mechanization of Proof: From 4-Color Theorem to Compiler Verification

2014.08.27 09:17 조회 수 : 2791

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.
번호 제목 글쓴이 날짜 조회 수
공지 Softeer 정기 코딩 테스트 안내 2021.12.06 5
공지 [삼성SDS] 2022년 동계 알고리즘 특강 안내 2021.12.01 40
공지 컴투스 대학생 서포터즈 컴투스 플레이어 7기 모집 2021.11.22 36
공지 Saccade Capital 채용공고 2021.11.11 82
공지 비스텔리젼스] AI/빅데이터 - Data Scientist 연구개발 채용 (병역특례 전문연 지원가능) 2021.10.01 349
공지 Data Scientist 경력/신입박사 채용 2021.09.27 392
공지 ㈜에프앤자산평가 채용공고(전문연구요원 채용) 2021.09.23 299
공지 (주)슈페릭스 Quant Researcher / Quant Developer 정규직 채용 2021.09.14 374
공지 [삼성SDS] 2021 연구장학생 선발 2021.09.02 368
공지 [LG전자] 2021년 CTO부문 국내외 우수 R&D 박사급 인재 채용 2021.08.10 458
공지 [현대엔지비] 2021 매치업 신에너지자동차 분야 교육생 모집 (~12.17) 2021.08.02 323
449 [알앤디잡]이공계인재 취업아카데미 참가신청 안내 2014.10.13 2518
448 ENEC 인턴십 및 채용 설명회 2014.10.13 3431
447 2015학년도 서울대학교 계산과학협동과정 신입생 모집 안내 2014.10.06 3749
446 해군사관학교 교수사관 (118기) 모집 안내 2014.10.02 4010
445 국가보안기술연구소 2014년도 하반기 정규직 채용 공고 2014.10.02 2493
444 Part-time Position at WorldQuant 2014.09.29 2871
443 ETRI부설 국가보안기술연구소 채용설명회 안내-9/22(월) 15:30~17:00 2014.09.17 3077
442 [SAP Korea] 채용 상담 & 채용 설명회 2014.09.16 2732
441 [산기협]9월 이공계 채용속보 2014.09.16 2600
440 NIMS 산업문제세미나-9/17(수) 4시 30분 PM 2014.09.11 2466
439 효성, 동부, LG Display 모집요강 2014.08.29 2469
438 [산기협]8월 이공계 채용속보 2014.08.29 2786
437 국가수리과학연구소(NIMS) 산업문제세미나-8/28(목) 11시 AM 2014.08.27 2766
436 국가수리과학연구소(NIMS) 초청세미나-8/27(수), 4:30 PM 2014.08.27 2744
» NIMS세미나 (8월 27일): 허충길 교수, Mechanization of Proof: From 4-Color Theorem to Compiler Verification 2014.08.27 2791
434 국가수리과학연구소(NIMS) 산업문제세미나-7/31(목) 오후 4시 30분 2014.07.25 3811
433 [채용공고] AXA Direct Korea - 2014 Summer Internship 2014.06.20 4203
432 국가수리과학연구소(NIMS) 산업문제 세미나-6/25(수) 오후 4시 2014.06.19 3366
431 HPCSS 2014 2014.06.17 3398
430 ETRI부설 국가보안기술연구소 2014년도 정규직 연구직, 기술직 채용공고 안내 (2014.06.17.~2014.07.01) 2014.06.17 6376
429 2014년도 해외유학장학생 및 중국유학장학생 선발 안내 2014.06.16 3206
428 국가수리과학연구소(NIMS) 콜로퀴엄 안내-2014. 06. 19. 2pm 2014.06.12 2617
427 국내 대형 증권사 신입 및 경력직 채용 공고 2014.06.11 2997
426 KISTI 첨단응용환경개발실 연수학생 모집 2014.06.10 2698
425 국가수리과학연구소(NIMS) 콜로퀴엄 안내-2014.05.30(금) 4:30 pm 2014.05.22 2968
424 국가수리과학연구소(NIMS) 산업문제세미나-5.21(수) 오후 4시 2014.05.13 2995
423 [바이오및뇌공학과 세미나] Sebastian Seung(MIT) 초청 2014.04.18 3483
422 2014년 상반기 동부그룹 대졸신입사원 모집요강 2014.04.16 3199
421 ㈜위메이드엔터테인먼트 DATA 분석 및 통계 전문가 모집 2014.04.15 3473
420 KAIST부설 한국과학영재학교 전임교원 채용 공고 2014.04.11 3444