취업 및 행사 정보

공지 시작  
공지 종료  
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
번호 제목 글쓴이 날짜 조회 수
공지 「삼성 청년 SW 아카데미」11기 교육생 모집! Coming Soon! 과사무실 2023.10.13 305
649 [OCI] 2017년 하반기 신입채용 모집 안내 [~10/19] 과사무실 2017.09.06 1007
648 SK 이노베이션 계열 "Job Talk"(하반기 채용설명회) file 과사무실 2017.09.05 2274
647 효성그룹 2017 하반기 신입사원 채용안내 file 과사무실 2017.09.05 1927
646 [현대오트론] 2017 하반기 현대오트론 대졸신입/인턴 공개모집 (~9/12) 과사무실 2017.09.04 1317
645 [한화토탈]2017 하반기 한화토탈 신입사원 채용 (~9/22) 과사무실 2017.09.04 1331
644 [LG디스플레이] 2017 하반기 대졸 정기채용 file 과사무실 2017.09.04 2250
643 [코오롱그룹] 2017 하반기 대졸 신입사원 모집 file 과사무실 2017.09.04 1434
642 [현대건설]2018 상반기 현대건설 신입사원 채용 과사무실 2017.09.01 1327
641 [회사설명회] 현대카드 과사무실 2017.09.01 1645
640 [한샘] 2017년 하반기 한샘 신입사원 공개채용 과사무실 2017.09.01 1053
639 현대카드 채용설명회 과사무실 2017.08.31 7187
638 [SK] 2017 하반기 신입사원 모집 캠퍼스 리크루팅 과사무실 2017.08.28 2032
637 [라인플러스] 2017 하반기 신입사원 채용 과사무실 2017.08.28 5275
636 [보스턴컨설팅그룹] 2017 ASSOCIATE CONSULTANT RECRUITING file 과사무실 2017.08.25 1833
635 [삼성카드] KAIST 재학생 대상 빅데이터 활용사례 특강 및 취업박람회 file 과사무실 2017.08.25 1285
634 [삼성SDS] 채용박람회 안내 과사무실 2017.08.23 2809
633 [한화큐셀]2017 하반기 신입사원 모집 file 과사무실 2017.08.23 1443
632 [현대자동차] 2017년 하반기 현대자동차 Job Fair 개최 과사무실 2017.08.10 1552
631 [네이버] 클로바 인공지능 아이디어 챌린지 공모 (7/19~8/6) 과사무실 2017.07.24 1160
630 SK하이닉스 '반도체 혁신 아이디어 공모전' 안내 과사무실 2017.07.20 1509
629 삼성전자 Foundry 사업부 리쿠르팅 과사무실 2017.07.10 4832
628 [삼성전자 종합기술원] 하반기 경력채용 공고 file 과사무실 2017.07.07 4724
627 [포스코그룹] 포스코/포스코대우 챌린지인턴십 모집 과사무실 2017.07.05 1521
626 '건설공제조합 2017년 신규직원 채용' 채용공고 안내드립니다. file 과사무실 2017.06.29 2930
625 [SK하이닉스]2017년 상반기 SK하이닉스 신입/경력 사원 모집(~7/7) file 과사무실 2017.06.26 1713
624 (주)사람인HR LAB 신입연구원 file 과사무실 2017.06.26 1618
623 [현대엠엔소프트] 17년 하반기 채용연계형 인턴사원 모집 과사무실 2017.06.26 2023
622 [카카오] 코드 페스티벌 접수 안내 (~8/4(금) 18시 까지) 과사무실 2017.06.19 1720
621 [율촌화학] 2017년 상반기 대졸신입 채용 과사무실 2017.06.19 1533
620 수리과학과 BK21플러스 사업단 연수연구원 초빙 공고(6월30일 마감) file 과사무실 2017.06.09 1359