취업 및 행사 정보

공지 시작  
공지 종료  
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 308
799 2019 Math in Paris Ph.D 펠로우십 프로그램 (프랑스대사관) 과사무실 2019.01.14 2125
798 2019년 하나금융융합기술원 인턴 채용~01/20(일) file 과사무실 2019.01.09 3913
797 (주)인엘씨테크놀러지 채용 공고 file 과사무실 2018.12.28 2852
796 [모집] 서울아산병원 박사급 인력 모집 과사무실 2018.12.24 2834
795 [아론티어] 학부생 인턴 채용(2019년도 단기 근로자 채용) file 과사무실 2018.12.19 3325
794 현대자동차 ICT본부 디지털혁신사업부 채용 file 윤향란 2018.12.11 2515
793 [LG CNS] 2019 Entrue 컨설팅 아카데미 동계 인턴 모집 file 과사무실 2018.11.29 2479
792 2019 LG CNS 인턴십 (동계 겨울방학) 모집 file 과사무실 2018.11.26 3337
791 [하나금융티아이] 하나금융 융합기술원 대학원생 인턴 모집 file 과사무실 2018.11.21 2273
790 삼성SDS가 준비한 기술 교류의 장, Techtonic 2018에 초대합니다. file 과사무실 2018.11.06 2102
789 산업수학 포럼 file 과사무실 2018.11.05 1770
788 산업수학 후속세대 문제해결 트레이닝 file 과사무실 2018.11.05 2077
787 The IBS Discrete Mathematics Group (DIMAG) Postdoctoral Research Fellowship 상일 2018.11.01 2604
786 [카카오] 인턴 (인턴 모집 기간 : 10/29~11/14) 과사무실 2018.10.30 3297
785 밀리만코리아 채용 file 과사무실 2018.10.24 2578
784 [고려아연] 2019년도 고려아연 및 계열사 신입사원 채용 과사무실 2018.10.24 1413
783 [삼성화재/회사설명회 개최] 10.26(금) 삼성화재-KAIST 회사설명회 과사무실 2018.10.22 1681
782 [NAVER] 네이버 개발자와 함께하는 해커톤! NAVER CAMPUS HACKDAY 2018 winter (~10월 31일까지 참가신청) file 과사무실 2018.10.17 1128
781 [현대엠엔소프트]2018 채용연계형 인턴사원 채용 file 과사무실 2018.10.15 1002
780 [원익그룹] 2018 원익그룹 하반기 신입사원 채용 file 과사무실 2018.10.02 1047
779 [하나금융그룹IT부문- 하나금융티아이] 신입사원 채용 file 과사무실 2018.10.01 1486
778 [이수그룹] 2019 이수그룹 신입사원 공개채용 (~10.22 까지) file 과사무실 2018.10.01 953
777 [아모레퍼시픽] 2018 하반기 아모레퍼시픽 신입사원 공개채용 file 과사무실 2018.09.27 1043
776 [게임빌컴투스 그룹] 2018년 게임빌·컴투스 그룹 공개채용 (~10/14) 모집 file 과사무실 2018.09.27 1042
775 !!모집일정확정!! [대림그룹] 2018년 하반기 신입사원 모집 file 과사무실 2018.09.27 1715
774 [메디톡스] 2018 메디톡스 신입사원 공개채용 file 과사무실 2018.09.27 919
773 [한온시스템] 2018 하반기 신입사원 모집 file 과사무실 2018.09.27 877
772 [동화그룹] 2018 하반기 대졸 신입사원 공개채용 file 과사무실 2018.09.19 1003
771 [LS그룹] 2018 하반기 LS그룹 대졸 신입사원 모집 file 과사무실 2018.09.14 935
770 [11번가] 2018 하반기 11번가 신입사원 채용 file 과사무실 2018.09.13 1349