취업 및 행사 정보

공지 시작  
공지 종료  
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 94
708 [현대오토에버]2018년 상반기 신입/인턴사원 공개채용 file 과사무실 2018.03.08 2099
707 [LG이노텍] 2018 상반기 대졸신입 채용 및 교내 채용상담 file 과사무실 2018.03.07 2906
706 [하이트진로] 2018 대졸 공채 및 공장견학설명회 과사무실 2018.03.07 4746
705 [한화케미칼] '18년 상반기 한화케미칼 신입사원 모집 file 과사무실 2018.03.05 2483
704 [LG CNS] IT Leadership Academy (2018 상반기 신입사원 채용) file 과사무실 2018.03.05 2209
703 [삼성SDI] 2018년 상반기 삼성SDI 공채/인턴 채용 file 과사무실 2018.03.05 2334
702 (국가보안기술연구소) 2018년도 1차 정규직(연구직, 기술직) 채용 공고(~3/7) file 과사무실 2018.02.22 7988
701 [삼성디스플레이] 한국과학기술원(수리과학과) 캠퍼스 리크루팅 file 과사무실 2018.02.22 2452
700 [월드퀀트] 글로벌 퀀트 회사 월드퀀트의 International Quant Championship 과사무실 2018.02.20 2634
699 (2차설명회)[SK하이닉스] 2018_상반기_SK하이닉스 TALK+ 수시 채용설명회 과사무실 2018.02.06 2450
698 [LG이노텍] CTO 광학기술 신입(석사이상) 사원 모집(~2/9) 과사무실 2018.02.02 2103
697 Streami Inc. is a blockchain startup working with leading financial service providers in Asia with the mission of bringing open, affordable, and efficient financial services. 과사무실 2018.02.01 4523
696 (1차설명회)[SK하이닉스] 2018_상반기_SK하이닉스 TALK+ 수시 채용설명회 모집 file 과사무실 2018.02.01 2457
695 [삼성디스플레이] 한국과학기술원(수리과학과) 대학생 초청행사 참가자 추천 공문 file 과사무실 2018.01.31 11854
694 삼성SDS 채용상담 및 SDS 잠실 Campus Tour 안내 과사무실 2018.01.26 2461
693 [LG CNS] 18년 동계인턴십 모집 file 과사무실 2018.01.11 2448
692 [LG CNS] 2018 동계 Smart IT 인턴십 모집(~18.01.14) 과사무실 2018.01.10 2280
691 [LG CNS] 2018 국내외 석박사 채용 file 과사무실 2017.12.22 2446
690 [LG CNS] 2018 동계 Smart IT 인턴십 모집 file 과사무실 2017.12.22 3493
689 [동화그룹] 2017 동화그룹 대졸신입 공개채용(~12/26) 과사무실 2017.12.18 2097
688 수리과학과 BK21플러스 사업단 연수연구원 초빙 공고(12월31일 마감) file 과사무실 2017.12.11 2224
687 [Event] KAIST-KIAS JOINT WORKSHOP IN THEORETICAL SCIENCES file 과사무실 2017.12.08 2086
686 2018년도 1학기 숭실대학교 수학과 연구중점교원 특별초빙 과사무실 2017.12.04 4934
685 [현대엠엔소프트] 2018년 채용연계형 인턴사원 모집[12.6~12.11] 과사무실 2017.12.04 2388
684 [LG전자]한국영업본부 채용연계형 인턴사원 5기 모집 과사무실 2017.12.04 3246
683 [LG전자]한국영업본부 채용연계형 인턴사원 5기 모집 과사무실 2017.12.04 1971
682 [한샘] '18년 상반기 신입SC 공개 채용 과사무실 2017.12.01 2074
681 미래에셋자산운용 금융공학/포트폴리오운용본부 인턴 채용 file 과사무실 2017.11.28 3113
680 [하포리서치코리아] 리서치 인턴 구인 과사무실 2017.11.23 3136
679 [삼성SDS] 석사·박사 채용 상담 file 과사무실 2017.11.17 8387