취업 및 행사 정보

공지 시작  
공지 종료  
NIMS 초청세미나


연사: 허충길 교수 (서울대 컴퓨터공학부 소프트웨어 이론 연구실)
일시: 8월 27일(수) 오후 4시 30분
장소: 국가수리과학연구소 수학원리응용센터 세미나실
제목: Mechanization of Proof: From 4-Color Theorem to Compiler Verification


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.


문의) 042-828-5811, wjeon@nims.re.kr
번호 제목 글쓴이 날짜 조회 수
공지 KAIST 수리과학과 4단계 BK21 연구교수 모집 공고 과사무실 2025.06.16 858
856 [채용공고] KAIST 확률 해석 및 응용 연구센터 연구교수 채용 (~12/27) [1] 과사무실 2019.12.13 5012
855 [모집] 제33기 한국수학올림피아드(KMO, Korean Mathematical Olympiad) 겨울학교 교육조교(대학생) file 과사무실 2019.11.21 6334
854 2019 카카오 개발자 겨울 인턴십에 도전해보세요! (~11/5) file 과사무실 2019.10.31 4705
853 [국가보안기술연구소] 2019년 2차 연구직/기술직 채용 file 과사무실 2019.09.26 4004
852 THE IBS DISCRETE MATHEMATICS GROUP (DIMAG) POSTDOCTORAL RESEARCH FELLOWSHIP (DUE: DEC. 1, 2019) 상일 2019.09.11 5572
851 2019년도 한국원자력연구원 정규직 공개채용 공고 file 과사무실 2019.09.03 5873
850 [현대모비스] 현대모비스 데이터사이언스팀에서는 데이터분석 및 AI분야의 전문가로 성장할 미래의 인재를 채용합니다. 과사무실 2019.09.03 3870
849 [전문연구요원] 무한 성장하는 쏘카와 함께할 여러분의 도전을 기다립니다. 과사무실 2019.09.02 3824
848 (채용) ㈜ 크립토랩 과사무실 2019.08.13 4635
847 2019년도 「청년 TLO 육성사업」사업 file 과사무실 2019.08.05 4660
846 2019 SK하이닉스 신입 박사급 특별채용(Fast Track) 설명회 과사무실 2019.07.19 3434
845 [채용 공고] 민족사관고등학교 시간강사 초빙공고 file 과사무실 2019.07.17 3744
844 [채용공고] KAIST 확률 해석 및 응용 연구센터 연수연구원(Post-doc) 채용 (~07/25) file 과사무실 2019.07.12 6812
843 [삼성디스플레이] 대학원생 대상 KAIST campus recruiting (7/1~7/3) file 과사무실 2019.06.28 6711
842 [한국산업인력공단] IDB 청년기술인재단 모집 연장 안내(~6.14) file 과사무실 2019.06.05 7184
841 IBS-CGP Mathematics Festival (July 7-12) file 과사무실 2019.05.31 4973
840 [케이원투자자문] 운용부문 신입직 채용 공고 file 과사무실 2019.05.27 4082
839 11기(2020년) 포스코사이언스펠로십 선발공고 file 과사무실 2019.05.23 6928
838 [한국산업인력공단] 미주개발은행(IDB) ICT 인재 채용 file 과사무실 2019.05.22 7399
837 [메리츠화재] 메리츠화재 데이터사이언스파트 채용 과사무실 2019.05.21 4670
836 [채용 공고] 민족사관고등학교 교사 또는 전임강사 초빙 공고 file 과사무실 2019.05.17 4204
835 (주)신세계 데이터엔지니어 경력직 채용 과사무실 2019.05.15 8185
834 삼성전자 삼성리서치 채용 설명회 과사무실 2019.05.13 10560
833 [한국무역협회-일본현지취업]일본 대기업 신입 엔지니어 채용 file 과사무실 2019.04.02 2997
832 [DB그룹] 2019년 상반기 신입공채 file 과사무실 2019.03.29 3878
831 [㈜한화 화약/방산] ㈜한화 화약/방산 2019년 상반기 신입사원 모집 file 과사무실 2019.03.26 3211
830 [한화파워시스템] 2019년 상반기 한화파워시스템 신입사원 채용 file 과사무실 2019.03.19 3914
829 [*채용공고] *LIG넥스원 -2019 상반기 신입/경력사원 채용 (~03/31) file 과사무실 2019.03.19 3704
828 [ASML] 2019 상반기 ASML Korea 신입/경력사원 채용 file 과사무실 2019.03.19 3001
827 [네이버] NAVER CAMPUS HACKDAY 2019 SUMMER 프로그램 file 과사무실 2019.03.18 4089