취업 및 행사 정보

공지 시작  
공지 종료  
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.
번호 제목 글쓴이 날짜 조회 수
공지 「삼성 청년 SW 아카데미」11기 교육생 모집! Coming Soon! 과사무실 2023.10.13 306
769 [포스코] 2018 하반기 포스코 연구원 채용 file 과사무실 2018.09.13 940
768 [삼양그룹] 2018 삼양그룹 신입사원 채용 과사무실 2018.09.12 1101
767 [한화에너지] 2018 하반기 신입사원 공개채용 ~9/27 과사무실 2018.09.12 1157
766 !!모집일정변경!! [대림그룹] 2018년 하반기 신입사원 모집 과사무실 2018.09.11 1187
765 금융예측모델(퀀트) 연구/개발 회사 하포리서치코리아 기술 및 기업설명회. file 과사무실 2018.09.10 1117
764 [GS SHOP] 2018 하반기 대졸 신입사원 공개채용 과사무실 2018.09.10 1096
763 [현대엔지니어링]2018 하반기 신입사원 공개채용 file 과사무실 2018.09.10 914
762 [포스코그룹] 2018년 하반기 채용 file 과사무실 2018.09.04 995
761 [LG유플러스] 2018 하반기 신입 채용/석박사 산학장학생 얼리버드 모집 과사무실 2018.09.03 1013
760 [BGF리테일] 2018년 하반기 BGF리테일 채용행사(캠퍼스리크루팅, 캠퍼스오디션) file 과사무실 2018.09.03 883
759 [뷰웍스] 카이스트 선배사원과 함께하는 채용 런치설명회 (전문연구요원지원 O) file 과사무실 2018.09.03 1106
758 [LS그룹] 2018 하반기 LS그룹 대졸 신입사원 모집 file 과사무실 2018.09.03 851
757 [대림그룹] 2018년 하반기 신입사원 모집 과사무실 2018.09.03 980
756 [LG서브원] 2018 하반기 신입사원 채용 과사무실 2018.09.03 921
755 [한화그룹] 2018년 하반기 한화종합화학 대졸 신입 채용 file 과사무실 2018.09.03 914
754 [한화시스템/시스템] 2018년 하반기 신입사원 모집 file 과사무실 2018.08.31 1160
753 [SK] 2018 하반기 신입사원 모집 캠퍼스 리크루팅 file 과사무실 2018.08.31 987
752 [한화큐셀] 본사 초청 잡페어 / 한화큐셀 2018년 하반기 신입사원 모집 file 과사무실 2018.08.31 1092
751 [현대오토에버] 2018 하반기 신입사원 공개채용 file 과사무실 2018.08.31 1031
750 [OCI] OCI 2018 하반기 신입채용 및 캠퍼스 리쿠르팅 file 과사무실 2018.08.31 907
749 [LG이노텍] 18 하 대졸신입사원 & 학사 산학장학생 9기 모집 file 과사무실 2018.08.31 1224
748 [KOLON] 2018년 하반기 코오롱그룹 대졸신입사원 상담회 file 과사무실 2018.08.31 1462
747 [LG화학] 2018 하반기 채용(신입/인턴/연구원/산학) 과사무실 2018.08.30 1841
746 [한화케미칼] 2018 하반기 한화케미칼 신입사원 모집 과사무실 2018.08.30 1935
745 [삼성전자DS부문] 채용 설명회 file 과사무실 2018.08.30 1254
744 2018년 셀트리온 그룹 하반기 공개채용』 8.31(금)~9.13 (목) 15시까지 file 과사무실 2018.08.30 997
743 [현대자동차] 2018 하반기 신입 및 인턴 채용_카이스트 R&D 우수인재 채용상담 및 설명회 file 과사무실 2018.08.30 1162
742 [현대제철] 2018 하반기 현대제철 신입사원/인턴십 채용 (~9/12) / 2018 현대제철 당진제철소 견학/직무 채용설명회 (9/7) 과사무실 2018.08.29 1669
741 [LG서브원] 2018 하반기 신입사원 채용 file 과사무실 2018.08.28 946
740 [현대자동차그룹] 2018 하반기 연구장학생&계약학과 모집 과사무실 2018.08.28 1396