취업 및 행사 정보

공지 시작  
공지 종료  
Date:August 27, 2014
Time: 4:30PM-5:30PM
Location: NIMS, CAMP seminar room (국가수리과학연구소 수학원리응용센터 세미나실)

[Title]

Mechanization of Proof: From 4-Color Theorem to Compiler Verification.

[Abstract]

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.

[Speaker]

Chung-Kil Hur (허충길)

[Short-Bio]

Chung-Kil Hur is an assistant professor in Department of Computer Science and Engineering at Seoul National University.  Previously he worked as a postdoctoral researcher at Microsoft Research Cambridge, Max Planck Institute for Software Systems (MPI-SWS) and Laboratoire PPS. He obtained a Ph.D. from University of Cambridge and a B.Sc. in Mathematics and in Computer Science from KAIST. He also received a bronze medal in the 35th International Mathematical Olympiad (IMO) in 1994.  His research interests are in software verification, interactive theorem proving, probabilistic programming and Beyesian inference.
번호 제목 글쓴이 날짜 조회 수
공지 「삼성 청년 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