취업 및 행사 정보

공지 시작  
공지 종료  
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
번호 제목 글쓴이 날짜 조회 수
공지 [넛지헬스케어_캐시워크] 데이터분석 담당 산업기능요원 모집 과사무실 2025.07.03 93
828 [ASML] 2019 상반기 ASML Korea 신입/경력사원 채용 file 과사무실 2019.03.19 3076
827 [네이버] NAVER CAMPUS HACKDAY 2019 SUMMER 프로그램 file 과사무실 2019.03.18 4179
826 [셀트리온 그룹] 『2019년 상반기 셀트리온 그룹 신입/경력 채용』 (~3.28 15:00까지) file 과사무실 2019.03.15 2605
825 (삼성생명) 2019년 상반기 신입사원 채용 file 과사무실 2019.03.15 3172
824 [ASML] 2019 상반기 ASML Korea 신입/경력사원 채용 file 과사무실 2019.03.14 3223
823 [한화케미칼] 한화케미칼 2019년 상반기 신입사원 모집 및 리쿠르팅 file 과사무실 2019.03.13 2959
822 [삼성SDS]학 · 석사 연구장학생 선발 file 과사무실 2019.03.12 5128
821 [포스코그룹] 2019년 상반기 포스코 그룹 신입/경력 사원 채용 과사무실 2019.03.12 2423
820 [공채] AJ '19년 상반기 대졸 신입사원 공채 file 과사무실 2019.03.12 3000
819 [SK실트론]2019 SK실트론 신입사원 수시채용 file 과사무실 2019.03.11 2583
818 [한화시스템/시스템] 2019년 상반기 신입사원 모집 및 캠퍼스 리쿠르팅 진행 과사무실 2019.03.11 3170
817 [롯데케미칼] 2019년 상반기 롯데케미칼 산학장학생 모집 과사무실 2019.03.11 2082
816 [삼양그룹] 2019 상반기 삼양그룹 신입사원 채용 file 과사무실 2019.03.11 1968
815 [한화큐셀 채용] KAIST 학생을 위한 런치설명회 사전신청 file 과사무실 2019.03.08 1867
814 [롯데케미칼] 2019년 상반기 롯데케미칼 산학장학생 모집 file 과사무실 2019.03.08 1982
813 [KT그룹] 2019년 상반기 신입/석박사/4차산업아카데미 인턴 채용 file 과사무실 2019.03.06 3236
812 [SK이노베이션] 2019 상반기 SK이노베이션 신입사원 모집 file 과사무실 2019.03.05 2001
811 네이버 Data Science Competition 2019 프로그램 file 과사무실 2019.03.04 2462
810 [롯데케미칼] 2019년 상반기 롯데케미칼 산학장학생 모집 file 과사무실 2019.03.04 1786
809 [현대자동차그룹] 2019년 상반기 현대자동차그룹 연구장학생/계약학과 모집 런치설명회 과사무실 2019.03.04 3055
808 LG화학/한국과학기술원(KAIST)] 2019 상반기 캠퍼스리쿠르팅 및 채용전형 과사무실 2019.03.04 2943
807 [삼성전자 DS부문] 2019 상반기 신입사원 모집 캠퍼스리크루팅 file 과사무실 2019.03.04 2042
806 [SK] 2019 상반기 인턴/신입사원 모집 캠퍼스 리크루팅 과사무실 2019.02.28 2339
805 2019 우리은행 이공계 석/박사 채용상담 과사무실 2019.02.28 2067
804 2019 상반기 SK주식회사 C&C 수시 채용 (~3월10일 24:00) file 과사무실 2019.02.27 2630
803 [현대오트론] 2019년 상반기 현대오트론 신입사원 채용 file 과사무실 2019.02.26 2903
802 [삼성SDS] 임원특강 file 과사무실 2019.02.26 2101
801 [현대자동차 재경본부] 2019년 현대자동차 재경본부 신입사원 상시채용(~2.26) 과사무실 2019.02.14 2109
800 2019 상반기 SK하이닉스 수시채용설명회 과사무실 2019.02.01 3753
799 2019 Math in Paris Ph.D 펠로우십 프로그램 (프랑스대사관) 과사무실 2019.01.14 3088