취업 및 행사 정보

공지 시작  
공지 종료  
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.
번호 제목 글쓴이 날짜 조회 수
공지 [IBK기업은행] 2025년 상반기 신입행원 공개채용 (~3/17, 10:00) 과사무실 2025.02.28 51
공지 [한화에어로스페이스] 파이브가이즈와 즐기는 KAIST 런치 채용설명회 과사무실 2025.02.28 49
공지 [(주) 보령] Global Investment Internship Program(GIIP) 인턴 채용 과사무실 2025.02.28 40
457 WorldQuant Quantitative Research Consultant 모집 file 과사무실 2014.10.24 4057
456 11.19 (수) 고등과학원 필즈 강연 과사무실 2014.10.22 3527
455 삼성전자 종합기술원 채용상담회 안내 file 과사무실 2014.10.20 3128
454 [산기협]이공계 10월 채용속보 file 과사무실 2014.10.20 2779
453 육군사관학교 교수사관 15기 모집 공고 file 과사무실 2014.10.16 4521
452 공군사관학교 교수사관 모집 file 과사무실 2014.10.15 5384
451 ㈜엔씨소프트 캠퍼스리크루팅 file 과사무실 2014.10.15 2992
450 제33회 전국 대학생 수학 경시대회 과사무실 2014.10.15 3832
449 [알앤디잡]이공계인재 취업아카데미 참가신청 안내 file 과사무실 2014.10.13 2871
448 ENEC 인턴십 및 채용 설명회 과사무실 2014.10.13 3824
447 2015학년도 서울대학교 계산과학협동과정 신입생 모집 안내 file 과사무실 2014.10.06 4134
446 해군사관학교 교수사관 (118기) 모집 안내 과사무실 2014.10.02 4489
445 국가보안기술연구소 2014년도 하반기 정규직 채용 공고 file 과사무실 2014.10.02 2838
444 Part-time Position at WorldQuant 과사무실 2014.09.29 3264
443 ETRI부설 국가보안기술연구소 채용설명회 안내-9/22(월) 15:30~17:00 과사무실 2014.09.17 3477
442 [SAP Korea] 채용 상담 & 채용 설명회 과사무실 2014.09.16 3060
441 [산기협]9월 이공계 채용속보 file 과사무실 2014.09.16 2927
440 NIMS 산업문제세미나-9/17(수) 4시 30분 PM file 과사무실 2014.09.11 2818
439 효성, 동부, LG Display 모집요강 file 과사무실 2014.08.29 2844
438 [산기협]8월 이공계 채용속보 file 과사무실 2014.08.29 3123
437 국가수리과학연구소(NIMS) 산업문제세미나-8/28(목) 11시 AM file 과사무실 2014.08.27 3195
436 국가수리과학연구소(NIMS) 초청세미나-8/27(수), 4:30 PM file 과사무실 2014.08.27 3078
» NIMS세미나 (8월 27일): 허충길 교수, Mechanization of Proof: From 4-Color Theorem to Compiler Verification 상일 2014.08.27 3125
434 국가수리과학연구소(NIMS) 산업문제세미나-7/31(목) 오후 4시 30분 file 과사무실 2014.07.25 4202
433 [채용공고] AXA Direct Korea - 2014 Summer Internship file 과사무실 2014.06.20 4607
432 국가수리과학연구소(NIMS) 산업문제 세미나-6/25(수) 오후 4시 file 과사무실 2014.06.19 3789
431 HPCSS 2014 file 관리자 2014.06.17 3774
430 ETRI부설 국가보안기술연구소 2014년도 정규직 연구직, 기술직 채용공고 안내 (2014.06.17.~2014.07.01) file 관리자 2014.06.17 6757
429 2014년도 해외유학장학생 및 중국유학장학생 선발 안내 과사무실 2014.06.16 3513
428 국가수리과학연구소(NIMS) 콜로퀴엄 안내-2014. 06. 19. 2pm file 과사무실 2014.06.12 2959