취업 및 행사 정보

공지 시작  
공지 종료  
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
번호 제목 글쓴이 날짜 조회 수
공지 KAIST 수리과학과 4단계 BK21 연구교수 모집 공고 과사무실 2025.06.16 841
465 2015년 LG유플러스 상반기 신입사원 채용 (Job Fair 신청 ~3월 8일(일)까지) file 과사무실 2015.03.04 2496
464 육군본부 회계원가비용분석병 모집 안내 file 과사무실 2015.02.02 4774
463 [산기협]1월 이공계 채용속보 게시 file 과사무실 2015.01.26 3561
462 2015년도 폴수학학교 교사 채용 공고(상시 모집) 과사무실 2015.01.20 8095
461 [수리과학연구소] 겨울학기 인턴십 모집 과사무실 2014.12.24 4087
460 1월26일(월) 고등과학원 대중강연 안내 (노벨상) 과사무실 2014.11.20 4261
459 11월26일(수) 고등과학원 대중 강연 안내 (필즈상) file 과사무실 2014.11.04 4487
458 학부생 연구원 모집(시스템생물학 및 바이오영감공학 연구실) file 과사무실 2014.10.29 3123
457 WorldQuant Quantitative Research Consultant 모집 file 과사무실 2014.10.24 4380
456 11.19 (수) 고등과학원 필즈 강연 과사무실 2014.10.22 3712
455 삼성전자 종합기술원 채용상담회 안내 file 과사무실 2014.10.20 3425
454 [산기협]이공계 10월 채용속보 file 과사무실 2014.10.20 3038
453 육군사관학교 교수사관 15기 모집 공고 file 과사무실 2014.10.16 4779
452 공군사관학교 교수사관 모집 file 과사무실 2014.10.15 5634
451 ㈜엔씨소프트 캠퍼스리크루팅 file 과사무실 2014.10.15 3266
450 제33회 전국 대학생 수학 경시대회 과사무실 2014.10.15 4092
449 [알앤디잡]이공계인재 취업아카데미 참가신청 안내 file 과사무실 2014.10.13 3152
448 ENEC 인턴십 및 채용 설명회 과사무실 2014.10.13 4132
447 2015학년도 서울대학교 계산과학협동과정 신입생 모집 안내 file 과사무실 2014.10.06 4379
446 해군사관학교 교수사관 (118기) 모집 안내 과사무실 2014.10.02 4806
445 국가보안기술연구소 2014년도 하반기 정규직 채용 공고 file 과사무실 2014.10.02 3145
444 Part-time Position at WorldQuant 과사무실 2014.09.29 3548
443 ETRI부설 국가보안기술연구소 채용설명회 안내-9/22(월) 15:30~17:00 과사무실 2014.09.17 3689
442 [SAP Korea] 채용 상담 & 채용 설명회 과사무실 2014.09.16 3315
441 [산기협]9월 이공계 채용속보 file 과사무실 2014.09.16 3151
440 NIMS 산업문제세미나-9/17(수) 4시 30분 PM file 과사무실 2014.09.11 3083
439 효성, 동부, LG Display 모집요강 file 과사무실 2014.08.29 3147
438 [산기협]8월 이공계 채용속보 file 과사무실 2014.08.29 3388
437 국가수리과학연구소(NIMS) 산업문제세미나-8/28(목) 11시 AM file 과사무실 2014.08.27 3465
» 국가수리과학연구소(NIMS) 초청세미나-8/27(수), 4:30 PM file 과사무실 2014.08.27 3372