취업 및 행사 정보

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
번호 제목 글쓴이 날짜 조회 수
공지 [NH투자증권] 고객지원센터 신입 상담직원 모집 (~01.22) 과사무실 2021.01.13 58
공지 [다쏘시스템코리아] 2021년 채용전환형 인턴십 모집 (~01.29) 과사무실 2021.01.12 53
공지 (주)한샘 키친&바스영업전문직(KD) 대규모 공개채용 (1월) (~1/13까지 접수) 과사무실 2021.01.08 45
공지 [Saccade Capital] Graduate Programme - Quant Analyst/Software Developer 과사무실 2020.12.16 160
공지 KAIST부설 한국과학영재학교 수리정보과학부 강사 모집 (~21.1.20) 과사무실 2020.12.10 277
공지 확률 해석 및 응용 연구센터 연수연구원(Post-Doc) 모집 공고 과사무실 2020.12.04 151
공지 삼성전자 DS 부문 생산기술연구소 온라인 리크루팅 안내 과사무실 2020.12.01 223
공지 KAIST 수리과학과 연수연구원 모집 공고 과사무실 2020.11.20 128
공지 KAIST 수리과학과 4단계 BK21 연구교수 모집 공고 과사무실 2020.11.16 155
공지 [TmaxGroup/R&D] 티맥스 R&D 개발 연구원 신입/경력 모집 (병역특례포함) 과사무실 2020.11.10 137
공지 [알파사이츠] 2020/2021 AlphaSights Associate 상시채용 과사무실 2020.10.27 93
470 [삼성전자] 자연계열 SCSA 채용설명회 과사무실 2015.03.16 2332
469 [한샘] 2015년 상반기 신입 공채 과사무실 2015.03.09 2264
468 [골프존그룹] 2015년 상반기 신입 공채 file 과사무실 2015.03.09 2192
467 [현대제철] 2015년 상반기 대졸신입사원 및 인턴십 채용 file 과사무실 2015.03.09 2326
466 [현대오토에버] 2015년 상반기 신입/하계 인턴 모집 file 과사무실 2015.03.09 1922
465 2015년 LG유플러스 상반기 신입사원 채용 (Job Fair 신청 ~3월 8일(일)까지) file 과사무실 2015.03.04 1918
464 육군본부 회계원가비용분석병 모집 안내 file 과사무실 2015.02.02 3898
463 [산기협]1월 이공계 채용속보 게시 file 과사무실 2015.01.26 2987
462 2015년도 폴수학학교 교사 채용 공고(상시 모집) 과사무실 2015.01.20 6642
461 [수리과학연구소] 겨울학기 인턴십 모집 과사무실 2014.12.24 3412
460 1월26일(월) 고등과학원 대중강연 안내 (노벨상) 과사무실 2014.11.20 3603
459 11월26일(수) 고등과학원 대중 강연 안내 (필즈상) file 과사무실 2014.11.04 3780
458 학부생 연구원 모집(시스템생물학 및 바이오영감공학 연구실) file 과사무실 2014.10.29 2484
457 WorldQuant Quantitative Research Consultant 모집 file 과사무실 2014.10.24 3630
456 11.19 (수) 고등과학원 필즈 강연 과사무실 2014.10.22 2553
455 삼성전자 종합기술원 채용상담회 안내 file 과사무실 2014.10.20 2754
454 [산기협]이공계 10월 채용속보 file 과사무실 2014.10.20 2429
453 육군사관학교 교수사관 15기 모집 공고 file 과사무실 2014.10.16 4066
452 공군사관학교 교수사관 모집 file 과사무실 2014.10.15 4932
451 ㈜엔씨소프트 캠퍼스리크루팅 file 과사무실 2014.10.15 2609
450 제33회 전국 대학생 수학 경시대회 과사무실 2014.10.15 3440
449 [알앤디잡]이공계인재 취업아카데미 참가신청 안내 file 과사무실 2014.10.13 2504
448 ENEC 인턴십 및 채용 설명회 과사무실 2014.10.13 3418
447 2015학년도 서울대학교 계산과학협동과정 신입생 모집 안내 file 과사무실 2014.10.06 3732
446 해군사관학교 교수사관 (118기) 모집 안내 과사무실 2014.10.02 3987
445 국가보안기술연구소 2014년도 하반기 정규직 채용 공고 file 과사무실 2014.10.02 2473
444 Part-time Position at WorldQuant 과사무실 2014.09.29 2845
443 ETRI부설 국가보안기술연구소 채용설명회 안내-9/22(월) 15:30~17:00 과사무실 2014.09.17 3063
442 [SAP Korea] 채용 상담 & 채용 설명회 과사무실 2014.09.16 2720
441 [산기협]9월 이공계 채용속보 file 과사무실 2014.09.16 2587