취업 및 행사 정보

공지 시작  
공지 종료  
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.
번호 제목 글쓴이 날짜 조회 수
공지 [넛지헬스케어_캐시워크] 데이터분석 담당 산업기능요원 모집 과사무실 2025.07.03 14
공지 KAIST 수리과학과 4단계 BK21 연구교수 모집 공고 과사무실 2025.06.16 1526
768 [삼양그룹] 2018 삼양그룹 신입사원 채용 과사무실 2018.09.12 2065
767 [한화에너지] 2018 하반기 신입사원 공개채용 ~9/27 과사무실 2018.09.12 2067
766 !!모집일정변경!! [대림그룹] 2018년 하반기 신입사원 모집 과사무실 2018.09.11 2080
765 금융예측모델(퀀트) 연구/개발 회사 하포리서치코리아 기술 및 기업설명회. file 과사무실 2018.09.10 1934
764 [GS SHOP] 2018 하반기 대졸 신입사원 공개채용 과사무실 2018.09.10 1973
763 [현대엔지니어링]2018 하반기 신입사원 공개채용 file 과사무실 2018.09.10 1794
762 [포스코그룹] 2018년 하반기 채용 file 과사무실 2018.09.04 1830
761 [LG유플러스] 2018 하반기 신입 채용/석박사 산학장학생 얼리버드 모집 과사무실 2018.09.03 1885
760 [BGF리테일] 2018년 하반기 BGF리테일 채용행사(캠퍼스리크루팅, 캠퍼스오디션) file 과사무실 2018.09.03 1737
759 [뷰웍스] 카이스트 선배사원과 함께하는 채용 런치설명회 (전문연구요원지원 O) file 과사무실 2018.09.03 1995
758 [LS그룹] 2018 하반기 LS그룹 대졸 신입사원 모집 file 과사무실 2018.09.03 1603
757 [대림그룹] 2018년 하반기 신입사원 모집 과사무실 2018.09.03 1758
756 [LG서브원] 2018 하반기 신입사원 채용 과사무실 2018.09.03 1736
755 [한화그룹] 2018년 하반기 한화종합화학 대졸 신입 채용 file 과사무실 2018.09.03 1699
754 [한화시스템/시스템] 2018년 하반기 신입사원 모집 file 과사무실 2018.08.31 1960
753 [SK] 2018 하반기 신입사원 모집 캠퍼스 리크루팅 file 과사무실 2018.08.31 1814
752 [한화큐셀] 본사 초청 잡페어 / 한화큐셀 2018년 하반기 신입사원 모집 file 과사무실 2018.08.31 1886
751 [현대오토에버] 2018 하반기 신입사원 공개채용 file 과사무실 2018.08.31 1813
750 [OCI] OCI 2018 하반기 신입채용 및 캠퍼스 리쿠르팅 file 과사무실 2018.08.31 1683
749 [LG이노텍] 18 하 대졸신입사원 & 학사 산학장학생 9기 모집 file 과사무실 2018.08.31 2032
748 [KOLON] 2018년 하반기 코오롱그룹 대졸신입사원 상담회 file 과사무실 2018.08.31 2238
747 [LG화학] 2018 하반기 채용(신입/인턴/연구원/산학) 과사무실 2018.08.30 2665
746 [한화케미칼] 2018 하반기 한화케미칼 신입사원 모집 과사무실 2018.08.30 2653
745 [삼성전자DS부문] 채용 설명회 file 과사무실 2018.08.30 2081
744 2018년 셀트리온 그룹 하반기 공개채용』 8.31(금)~9.13 (목) 15시까지 file 과사무실 2018.08.30 1759
743 [현대자동차] 2018 하반기 신입 및 인턴 채용_카이스트 R&D 우수인재 채용상담 및 설명회 file 과사무실 2018.08.30 1978
742 [현대제철] 2018 하반기 현대제철 신입사원/인턴십 채용 (~9/12) / 2018 현대제철 당진제철소 견학/직무 채용설명회 (9/7) 과사무실 2018.08.29 2512
741 [LG서브원] 2018 하반기 신입사원 채용 file 과사무실 2018.08.28 1901
740 [현대자동차그룹] 2018 하반기 연구장학생&계약학과 모집 과사무실 2018.08.28 2304
739 [삼성SDS] 임원 IT Trend 특강 참석자 모집 (~8/30) 과사무실 2018.08.28 2519