취업 및 행사 정보

공지 시작  
공지 종료  
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.
번호 제목 글쓴이 날짜 조회 수
공지 [KAIST 전기및전자공학부] KAIST 하정석 교수님 연구실(CoCoA) 학부연구원 모집 안내 과사무실 2025.07.15 4
공지 [넛지헬스케어_캐시워크] 데이터분석 담당 산업기능요원 모집 과사무실 2025.07.03 100
679 [삼성SDS] 석사·박사 채용 상담 file 과사무실 2017.11.17 8387
678 [삼성SDS] 석사·박사 채용 상담 과사무실 2017.11.16 3820
677 [EY한영/Ernst&Young] 채용 설명회 및 공개채용 file 과사무실 2017.11.08 2464
676 [조교 모집] 어른의 수학- 조교를 모집합니다. 과사무실 2017.11.03 2623
675 [대한유화(주)] 2017 대졸 신입,경력사원 공채 file 과사무실 2017.10.23 2113
674 엔씨소프트 AI Research 분야 공개 채용 과사무실 2017.10.17 2461
673 2017 [한솔그룹] 하반기 대졸 신입사원 모집 과사무실 2017.10.10 2183
672 [금호석유화학] 2017 신입행원 모집 file 과사무실 2017.10.10 2413
671 [대림그룹] '17(하) 신입사원 공개채용 과사무실 2017.10.10 1871
670 [모집직무수정][동화그룹] 2017 하반기 대졸신입공채 과사무실 2017.10.10 2238
669 [고영테크놀러지] 2017 고영테크놀러지 하반기 공개 채용 file 과사무실 2017.09.25 2027
668 [원익그룹] 2017 원익그룹 신입공채 및 캠퍼스 리쿠르팅 과사무실 2017.09.25 2135
667 [동화그룹] 2017 하반기 대졸신입공채 과사무실 2017.09.25 2174
666 [원익그룹] 2017 원익그룹 신입공채 과사무실 2017.09.25 1949
665 삼성전자 종합기술원 채용 상담회 과사무실 2017.09.22 2105
664 [한온시스템]2017 하반기 신입 채용상담회 과사무실 2017.09.20 2444
663 [한화기계]2017 하반기 한화기계 신입사원 채용 (~9/22) 과사무실 2017.09.18 2145
662 [유니드컴즈] 기업부설연구소 연구원 모집공고 file 과사무실 2017.09.15 5136
661 [코오롱그룹] 2017 하반기 대졸 신입사원 모집 과사무실 2017.09.14 1814
660 [동원그룹]2017 하반기 신입사원 채용 과사무실 2017.09.14 2288
659 [WorldQuant] 퀀트 연구원(Quantitative Researcher) 채용공고 및 캠퍼스 리크루팅 과사무실 2017.09.14 4088
658 (일화)채용정보 과사무실 2017.09.14 1839
657 2017년 하반기 삼성증권 신입 채용 file 과사무실 2017.09.12 4311
656 [대원제약] 2017 하반기 공개 채용 과사무실 2017.09.12 4381
655 2017 하반기 삼양그룹 신입사원 모집 및 리크루팅 과사무실 2017.09.11 2158
654 [GS SHOP] 2017년 GS SHOP 대졸 신입사원 공개채용 과사무실 2017.09.11 2087
653 [현대자동차그룹] 자동차 햅틱 기술 아이디어 공모전 (~10/13) 과사무실 2017.09.11 2113
652 코스닥 코넥스 상장기업 취업박람회 과사무실 2017.09.08 3222
651 [한미약품] 채용정보 과사무실 2017.09.07 4532
650 [SK] 2017 하반기 신입사원 모집 캠퍼스 리크루팅 홍보 과사무실 2017.09.07 2386