취업 및 행사 정보

공지 시작  
공지 종료  
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 94
858 확률/머신러닝/크라우드소싱 전공 연구원 채용 (AI학습데이터 스타트업 셀렉트스타) 과사무실 2020.01.08 2781
857 [채용공고] KAIST 확률 해석 및 응용 연구센터 연수연구원(Postdoc/연구원) 채용 (~12/27) file 과사무실 2019.12.13 6337
856 [채용공고] KAIST 확률 해석 및 응용 연구센터 연구교수 채용 (~12/27) [1] 과사무실 2019.12.13 5159
855 [모집] 제33기 한국수학올림피아드(KMO, Korean Mathematical Olympiad) 겨울학교 교육조교(대학생) file 과사무실 2019.11.21 6415
854 2019 카카오 개발자 겨울 인턴십에 도전해보세요! (~11/5) file 과사무실 2019.10.31 4794
853 [국가보안기술연구소] 2019년 2차 연구직/기술직 채용 file 과사무실 2019.09.26 4104
852 THE IBS DISCRETE MATHEMATICS GROUP (DIMAG) POSTDOCTORAL RESEARCH FELLOWSHIP (DUE: DEC. 1, 2019) 상일 2019.09.11 5665
851 2019년도 한국원자력연구원 정규직 공개채용 공고 file 과사무실 2019.09.03 5945
850 [현대모비스] 현대모비스 데이터사이언스팀에서는 데이터분석 및 AI분야의 전문가로 성장할 미래의 인재를 채용합니다. 과사무실 2019.09.03 3956
849 [전문연구요원] 무한 성장하는 쏘카와 함께할 여러분의 도전을 기다립니다. 과사무실 2019.09.02 3916
848 (채용) ㈜ 크립토랩 과사무실 2019.08.13 4715
847 2019년도 「청년 TLO 육성사업」사업 file 과사무실 2019.08.05 4750
846 2019 SK하이닉스 신입 박사급 특별채용(Fast Track) 설명회 과사무실 2019.07.19 3491
845 [채용 공고] 민족사관고등학교 시간강사 초빙공고 file 과사무실 2019.07.17 3815
844 [채용공고] KAIST 확률 해석 및 응용 연구센터 연수연구원(Post-doc) 채용 (~07/25) file 과사무실 2019.07.12 6887
843 [삼성디스플레이] 대학원생 대상 KAIST campus recruiting (7/1~7/3) file 과사무실 2019.06.28 6786
842 [한국산업인력공단] IDB 청년기술인재단 모집 연장 안내(~6.14) file 과사무실 2019.06.05 7264
841 IBS-CGP Mathematics Festival (July 7-12) file 과사무실 2019.05.31 5065
840 [케이원투자자문] 운용부문 신입직 채용 공고 file 과사무실 2019.05.27 4173
839 11기(2020년) 포스코사이언스펠로십 선발공고 file 과사무실 2019.05.23 6990
838 [한국산업인력공단] 미주개발은행(IDB) ICT 인재 채용 file 과사무실 2019.05.22 7490
837 [메리츠화재] 메리츠화재 데이터사이언스파트 채용 과사무실 2019.05.21 4747
836 [채용 공고] 민족사관고등학교 교사 또는 전임강사 초빙 공고 file 과사무실 2019.05.17 4313
835 (주)신세계 데이터엔지니어 경력직 채용 과사무실 2019.05.15 8265
834 삼성전자 삼성리서치 채용 설명회 과사무실 2019.05.13 10645
833 [한국무역협회-일본현지취업]일본 대기업 신입 엔지니어 채용 file 과사무실 2019.04.02 3079
832 [DB그룹] 2019년 상반기 신입공채 file 과사무실 2019.03.29 3980
831 [㈜한화 화약/방산] ㈜한화 화약/방산 2019년 상반기 신입사원 모집 file 과사무실 2019.03.26 3274
830 [한화파워시스템] 2019년 상반기 한화파워시스템 신입사원 채용 file 과사무실 2019.03.19 4000
829 [*채용공고] *LIG넥스원 -2019 상반기 신입/경력사원 채용 (~03/31) file 과사무실 2019.03.19 3787