취업 및 행사 정보

공지 시작  
공지 종료  
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 308
1219 [한국자동차연구원] 2023년 상반기 정규직 채용 상담회 (3/30) 과사무실 2023.03.29 73
1218 [두산밥캣] 2023 상반기 신입 인턴 채용 (~4/7) 과사무실 2023.03.27 93
1217 [HD현대] 2023 상반기 건설기계 3사 신입사원 채용 (~4/7) 과사무실 2023.03.22 90
1216 [롯데케미칼] 2023년 3월 롯데케미칼 첨단소재사업 신입사원 채용 일반전형 (~4/2) 과사무실 2023.03.22 76
1215 [아모레퍼시픽] 2023년 상반기 신입사원 수시채용 (~4/5) 과사무실 2023.03.21 74
1214 [LX인터내셔널] 신입사원 채용(채용연계형 인턴십) 과사무실 2023.03.21 76
1213 [(주)한화/글로벌] 2023 신입사원 채용 (~3월 26일) 과사무실 2023.03.21 69
1212 NH농협은행 5급 경력직 신규직원 채용 과사무실 2023.03.17 119
1211 삼성전자 DS부문 혁신센터에서 2023년 상반기 3급 공개채용 과사무실 2023.03.14 506
1210 [공군사관학교 수학과] 151기 교수사관 모집 관련 홍보 과사무실 2023.03.10 84
1209 [한국여성과학기술인육성재단] 이공계 여학생 대상 멘토링 프로그램 (~4/1) 과사무실 2023.03.10 70
1208 [삼성웰스토리] 2023년 상반기 신입사원 공개채용 (~3/23) 과사무실 2023.03.10 79
1207 [롯데그룹] 3월 롯데 채용 및 수요 커리어 멘토링 프로그램 안내 과사무실 2023.03.09 66
1206 [LIG넥스원] 2023 상반기 LIG넥스원 수시채용 과사무실 2023.03.08 79
1205 [현대카드/현대커머셜] 2023 Internship (~3/20) 과사무실 2023.03.06 77
1204 [포스코그룹] '23년 상반기 포스코그룹 신입/경력 채용 (~3/22(수), 15시) 과사무실 2023.03.03 72
1203 2023년 상반기 RIST 공개 채용 | 행정직 | (~3/22) 과사무실 2023.03.02 79
1202 2023년 상반기 RIST 공개 채용 | 기술직 | (~3/22) file 과사무실 2023.03.02 79
1201 2023년 상반기 RIST 공개 채용 | 연구직 | (~3/22) file 과사무실 2023.03.02 77
1200 2023년도 한국여성수리과학회 2기 학생기자단 모집 (~4.15) file 과사무실 2023.02.27 78
1199 삼성디스플레이 23년도 상반기 박사채용 및 박사장학생 모집 (~3.17) file 과사무실 2023.02.27 93
1198 [LIG넥스원] 2023 상반기 LIG넥스원 수시채용 과사무실 2023.02.20 84
1197 [한화시스템] [수정] 2023 방산부문 신입사원 채용 (~3/1) file 과사무실 2023.02.20 97
1196 프레스토투자자문 Algorithmic Trader 채용공고(~3/31) file 과사무실 2023.02.07 370
1195 크립토햅 회사 설명회 file 과사무실 2022.11.01 212
1194 IBS-SDU Autumn Course on Extremal Combinatorics DIMAG 2022.09.25 151
1193 2022년도 자연과학연구소 연구교원 채용공고 file 과사무실 2022.09.02 225
1192 [삼성SDS] KAIST 박사채용 리크루팅 file 과사무실 2022.09.02 212
1191 2022년 AI 융합기술을 활용한 의료·산업수학 문제 해결 워크숍 과사무실 2022.08.29 181
1190 [웨이브릿지] 정규직(신입)/전문연구요원 모집 (Quant 직군) 과사무실 2022.05.20 360