취업 및 행사 정보

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.
번호 제목 글쓴이 날짜 조회 수
공지 [LS그룹] 2021년 대졸 신입사원 공개채용(~10월 15일) 과사무실 2021.10.14 18
공지 [차바이오그룹] 2021 하반기 차바이오그룹 신입·경력 공개채용 ( ~ 11/5) 과사무실 2021.10.13 23
공지 [차병원] 2021 하반기 차병원 신입·경력 공개채용 ( ~ 11/5) 과사무실 2021.10.13 16
공지 [안국약품] 2021 하반기 안국약품 공개채용 및 채용 설명회 진행 ( ~ 10/17) 과사무실 2021.10.12 35
공지 [기한 연장] [신영증권] 2021년 하반기 공개채용 (~10/18) 과사무실 2021.10.12 20
공지 비스텔리젼스] AI/빅데이터 - Data Scientist 연구개발 채용 (병역특례 전문연 지원가능) 과사무실 2021.10.01 148
공지 [현대자동차그룹] 2021 현대자동차 계약학과 모집(~10.18(월)) 과사무실 2021.10.01 118
공지 [코닝정밀소재] 2021년 코닝정밀소재 정규직 신입채용 (~10/20) 과사무실 2021.10.01 114
공지 Data Scientist 경력/신입박사 채용 과사무실 2021.09.27 184
공지 ㈜에프앤자산평가 채용공고(전문연구요원 채용) 과사무실 2021.09.23 115
공지 한국과학기술원 부설 한국과학영재학교 전임 교원 초빙 공고 KSA Full Time Faculty Recruitment 과사무실 2021.09.17 207
공지 (주)슈페릭스 Quant Researcher / Quant Developer 정규직 채용 과사무실 2021.09.14 150
공지 [삼성SDS] 2021 연구장학생 선발 과사무실 2021.09.02 167
공지 [LG전자] 2021년 CTO부문 국내외 우수 R&D 박사급 인재 채용 과사무실 2021.08.10 230
공지 [현대엔지비] 2021 매치업 신에너지자동차 분야 교육생 모집 (~12.17) 과사무실 2021.08.02 140
466 [현대오토에버] 2015년 상반기 신입/하계 인턴 모집 file 과사무실 2015.03.09 1922
465 2015년 LG유플러스 상반기 신입사원 채용 (Job Fair 신청 ~3월 8일(일)까지) file 과사무실 2015.03.04 1919
464 육군본부 회계원가비용분석병 모집 안내 file 과사무실 2015.02.02 3932
463 [산기협]1월 이공계 채용속보 게시 file 과사무실 2015.01.26 2994
462 2015년도 폴수학학교 교사 채용 공고(상시 모집) 과사무실 2015.01.20 6766
461 [수리과학연구소] 겨울학기 인턴십 모집 과사무실 2014.12.24 3414
460 1월26일(월) 고등과학원 대중강연 안내 (노벨상) 과사무실 2014.11.20 3604
459 11월26일(수) 고등과학원 대중 강연 안내 (필즈상) file 과사무실 2014.11.04 3785
458 학부생 연구원 모집(시스템생물학 및 바이오영감공학 연구실) file 과사무실 2014.10.29 2488
457 WorldQuant Quantitative Research Consultant 모집 file 과사무실 2014.10.24 3662
456 11.19 (수) 고등과학원 필즈 강연 과사무실 2014.10.22 2632
455 삼성전자 종합기술원 채용상담회 안내 file 과사무실 2014.10.20 2773
454 [산기협]이공계 10월 채용속보 file 과사무실 2014.10.20 2431
453 육군사관학교 교수사관 15기 모집 공고 file 과사무실 2014.10.16 4081
452 공군사관학교 교수사관 모집 file 과사무실 2014.10.15 4951
451 ㈜엔씨소프트 캠퍼스리크루팅 file 과사무실 2014.10.15 2616
450 제33회 전국 대학생 수학 경시대회 과사무실 2014.10.15 3442
449 [알앤디잡]이공계인재 취업아카데미 참가신청 안내 file 과사무실 2014.10.13 2506
448 ENEC 인턴십 및 채용 설명회 과사무실 2014.10.13 3421
447 2015학년도 서울대학교 계산과학협동과정 신입생 모집 안내 file 과사무실 2014.10.06 3734
446 해군사관학교 교수사관 (118기) 모집 안내 과사무실 2014.10.02 3999
445 국가보안기술연구소 2014년도 하반기 정규직 채용 공고 file 과사무실 2014.10.02 2476
444 Part-time Position at WorldQuant 과사무실 2014.09.29 2861
443 ETRI부설 국가보안기술연구소 채용설명회 안내-9/22(월) 15:30~17:00 과사무실 2014.09.17 3068
442 [SAP Korea] 채용 상담 & 채용 설명회 과사무실 2014.09.16 2720
441 [산기협]9월 이공계 채용속보 file 과사무실 2014.09.16 2588
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