취업 및 행사 정보

공지 시작  
공지 종료  
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 14
공지 KAIST 수리과학과 4단계 BK21 연구교수 모집 공고 과사무실 2025.06.16 1756
768 [삼양그룹] 2018 삼양그룹 신입사원 채용 과사무실 2018.09.12 2077
767 [한화에너지] 2018 하반기 신입사원 공개채용 ~9/27 과사무실 2018.09.12 2078
766 !!모집일정변경!! [대림그룹] 2018년 하반기 신입사원 모집 과사무실 2018.09.11 2098
765 금융예측모델(퀀트) 연구/개발 회사 하포리서치코리아 기술 및 기업설명회. file 과사무실 2018.09.10 1953
764 [GS SHOP] 2018 하반기 대졸 신입사원 공개채용 과사무실 2018.09.10 1990
763 [현대엔지니어링]2018 하반기 신입사원 공개채용 file 과사무실 2018.09.10 1812
762 [포스코그룹] 2018년 하반기 채용 file 과사무실 2018.09.04 1843
761 [LG유플러스] 2018 하반기 신입 채용/석박사 산학장학생 얼리버드 모집 과사무실 2018.09.03 1899
760 [BGF리테일] 2018년 하반기 BGF리테일 채용행사(캠퍼스리크루팅, 캠퍼스오디션) file 과사무실 2018.09.03 1758
759 [뷰웍스] 카이스트 선배사원과 함께하는 채용 런치설명회 (전문연구요원지원 O) file 과사무실 2018.09.03 2015
758 [LS그룹] 2018 하반기 LS그룹 대졸 신입사원 모집 file 과사무실 2018.09.03 1620
757 [대림그룹] 2018년 하반기 신입사원 모집 과사무실 2018.09.03 1770
756 [LG서브원] 2018 하반기 신입사원 채용 과사무실 2018.09.03 1753
755 [한화그룹] 2018년 하반기 한화종합화학 대졸 신입 채용 file 과사무실 2018.09.03 1718
754 [한화시스템/시스템] 2018년 하반기 신입사원 모집 file 과사무실 2018.08.31 1976
753 [SK] 2018 하반기 신입사원 모집 캠퍼스 리크루팅 file 과사무실 2018.08.31 1833
752 [한화큐셀] 본사 초청 잡페어 / 한화큐셀 2018년 하반기 신입사원 모집 file 과사무실 2018.08.31 1899
751 [현대오토에버] 2018 하반기 신입사원 공개채용 file 과사무실 2018.08.31 1829
750 [OCI] OCI 2018 하반기 신입채용 및 캠퍼스 리쿠르팅 file 과사무실 2018.08.31 1697
749 [LG이노텍] 18 하 대졸신입사원 & 학사 산학장학생 9기 모집 file 과사무실 2018.08.31 2046
748 [KOLON] 2018년 하반기 코오롱그룹 대졸신입사원 상담회 file 과사무실 2018.08.31 2250
747 [LG화학] 2018 하반기 채용(신입/인턴/연구원/산학) 과사무실 2018.08.30 2679
746 [한화케미칼] 2018 하반기 한화케미칼 신입사원 모집 과사무실 2018.08.30 2668
745 [삼성전자DS부문] 채용 설명회 file 과사무실 2018.08.30 2097
744 2018년 셀트리온 그룹 하반기 공개채용』 8.31(금)~9.13 (목) 15시까지 file 과사무실 2018.08.30 1776
743 [현대자동차] 2018 하반기 신입 및 인턴 채용_카이스트 R&D 우수인재 채용상담 및 설명회 file 과사무실 2018.08.30 2000
742 [현대제철] 2018 하반기 현대제철 신입사원/인턴십 채용 (~9/12) / 2018 현대제철 당진제철소 견학/직무 채용설명회 (9/7) 과사무실 2018.08.29 2529
741 [LG서브원] 2018 하반기 신입사원 채용 file 과사무실 2018.08.28 1915
740 [현대자동차그룹] 2018 하반기 연구장학생&계약학과 모집 과사무실 2018.08.28 2323
739 [삼성SDS] 임원 IT Trend 특강 참석자 모집 (~8/30) 과사무실 2018.08.28 2540