취업 및 행사 정보

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.
번호 제목 글쓴이 날짜 조회 수
공지 [포스코건설] 2021 상반기 채용연계형 인턴 신입 채용 (~5.3 13시) 과사무실 2021.04.14 6
공지 [ABInBev Korea 오비맥주] 2021년 상반기 GMT/SET Summer Intern 모집 (~4/20 기간 연장) 과사무실 2021.04.14 6
공지 [현대자동차] 현대자동차 연구개발본부 전 부문 경력 인재 모집(~04.28) 과사무실 2021.04.14 13
공지 [WISET] WISET-한국 3M 글로벌 멘토링 멘티 모집(~5/2) 과사무실 2021.04.14 4
공지 [현대글로비스] 2021 신입사원 채용 과사무실 2021.04.09 31
공지 [LG화학] 4월 R&D 신입사원 모집(석/박사) 및 채용설명회 안내 과사무실 2021.04.09 28
공지 [삼양그룹] 2021 상반기 삼양그룹 신입사원 모집(~4.18) 과사무실 2021.04.09 19
공지 아이들이 자신만의 프로젝트를 자유롭게 펼치는 커뮤니티 공간, <프로젝토리> 운영 크루 모집 과사무실 2021.04.09 15
공지 2021년 4월 SK텔레콤 카이스트 Junior Talent 채용설명회 과사무실 2021.04.08 37
공지 [롯데그룹] 21년 상반기 상시채용 <ZOOM TALK> 안내 과사무실 2021.04.06 37
공지 [DB손해보험]2021년 DB손해보험 상반기 신입사원 모집(~4.15 17시) 과사무실 2021.04.05 37
공지 (주)한샘 키친&바스영업전문직(KD) 대규모 공개채용 (21년 4월) (~4/14까지 접수) 과사무실 2021.04.05 20
공지 [ABInBev Korea 오비맥주] 2021년 상반기 GMT/SET Summer Intern 모집 (~4/20 기간 연장) 과사무실 2021.04.05 28
공지 「전라남도 해외유학생」 선발 공고(~4.15 기간 연장) 과사무실 2021.04.01 32
공지 [WISET] 여대학(원)생을 위한 '글로벌 크로스 멘토링' 모집 공고 홍보 과사무실 2021.03.31 33
공지 <2021 이화-루스 온라인 국제세미나: 지평넓히기>에 초대합니다 과사무실 2021.03.30 38
공지 [SK이노베이션] 2021 SK이노베이션 신입사원 모집 (~4/16 (금), 24시) 과사무실 2021.03.30 32
공지 「전라남도 해외유학생」 선발 공고 과사무실 2021.03.23 42
공지 [시높시스코리아] 2021년 채용전환형 인턴 모집 안내 (~ 4월 30일 마감) 과사무실 2021.03.22 33
공지 SKI Data Scientist 채용 과사무실 2021.03.22 84
공지 [한국여성과학기술인지원센터] 이공계 여자 대학(원)생 대상 취업/진학 멘토링 프로그램 과사무실 2021.03.18 33
443 ETRI부설 국가보안기술연구소 채용설명회 안내-9/22(월) 15:30~17:00 과사무실 2014.09.17 3065
442 [SAP Korea] 채용 상담 & 채용 설명회 과사무실 2014.09.16 2720
441 [산기협]9월 이공계 채용속보 file 과사무실 2014.09.16 2587
440 NIMS 산업문제세미나-9/17(수) 4시 30분 PM file 과사무실 2014.09.11 2457
439 효성, 동부, LG Display 모집요강 file 과사무실 2014.08.29 2458
438 [산기협]8월 이공계 채용속보 file 과사무실 2014.08.29 2775
437 국가수리과학연구소(NIMS) 산업문제세미나-8/28(목) 11시 AM file 과사무실 2014.08.27 2752
436 국가수리과학연구소(NIMS) 초청세미나-8/27(수), 4:30 PM file 과사무실 2014.08.27 2728
» NIMS세미나 (8월 27일): 허충길 교수, Mechanization of Proof: From 4-Color Theorem to Compiler Verification 상일 2014.08.27 2774
434 국가수리과학연구소(NIMS) 산업문제세미나-7/31(목) 오후 4시 30분 file 과사무실 2014.07.25 3790
433 [채용공고] AXA Direct Korea - 2014 Summer Internship file 과사무실 2014.06.20 4181
432 국가수리과학연구소(NIMS) 산업문제 세미나-6/25(수) 오후 4시 file 과사무실 2014.06.19 3356
431 HPCSS 2014 file 관리자 2014.06.17 3389
430 ETRI부설 국가보안기술연구소 2014년도 정규직 연구직, 기술직 채용공고 안내 (2014.06.17.~2014.07.01) file 관리자 2014.06.17 6356
429 2014년도 해외유학장학생 및 중국유학장학생 선발 안내 과사무실 2014.06.16 3186
428 국가수리과학연구소(NIMS) 콜로퀴엄 안내-2014. 06. 19. 2pm file 과사무실 2014.06.12 2602
427 국내 대형 증권사 신입 및 경력직 채용 공고 과사무실 2014.06.11 2973
426 KISTI 첨단응용환경개발실 연수학생 모집 file 과사무실 2014.06.10 2682
425 국가수리과학연구소(NIMS) 콜로퀴엄 안내-2014.05.30(금) 4:30 pm 과사무실 2014.05.22 2949
424 국가수리과학연구소(NIMS) 산업문제세미나-5.21(수) 오후 4시 file 과사무실 2014.05.13 2974
423 [바이오및뇌공학과 세미나] Sebastian Seung(MIT) 초청 과사무실 2014.04.18 3468
422 2014년 상반기 동부그룹 대졸신입사원 모집요강 file 과사무실 2014.04.16 3178
421 ㈜위메이드엔터테인먼트 DATA 분석 및 통계 전문가 모집 과사무실 2014.04.15 3456
420 KAIST부설 한국과학영재학교 전임교원 채용 공고 file 과사무실 2014.04.11 3422
419 KMRS IT Lounge Opening Ceremony file 과사무실 2014.04.10 2649
418 국가수리과학연구소(NIMS) 콜로퀴엄 안내-2014.04.16(수) 4:30 pm 과사무실 2014.04.04 2836
417 2014 Qualcomm IT Tour file 과사무실 2014.03.31 3769
416 『두산중공업 2014년 채용연계 인턴십 모집 및 Campus Recruiting 공고』 file 과사무실 2014.03.18 3924
415 British council Researchers Links workshop on soft matter(NIMS) file 과사무실 2014.03.14 3949
414 국가수리과학연구소 채용 관련 안내 file 과사무실 2014.03.14 3333