Extra Form
Lecturer 허충길
Dept. 서울대 컴퓨터공학부
date Apr 15, 2015

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.

Attachment '1'
List of Articles
Category Subject Dept. Lecturer
Math Colloquia <2020년도 젊은 과학자상 수상 기념강연> Metastability of stochastic systems file 서울대학교 서인석
Math Colloquia <정년퇴임 기념강연> 작용소대수와 양자정보이론 file 서울대학교 계승혁
Math Colloquia From mirror symmetry to enumerative geometry file 서울대학교 오정석
Math Colloquia <정년퇴임 기념강연> The Elements of Euclid file 서울대/광주과학기술원 김홍종
Math Colloquia Mechanization of proof: from 4-Color theorem to compiler verification file 서울대 컴퓨터공학부 허충길
Math Colloquia <학부생을 위한 ɛ 강연> 4차 산업혁명, 글로벌 디지털 혁신과 일자리 전쟁, 대학의 역할 file 서울대 전기정보공학부, 빅데이터연구원 원장 차상균
Math Colloquia Recommendation system and matrix completion: SVD and its applications (학부생을 위한 강연) file 서울대 전기공학부 정교민
Math Colloquia Freudenthal medal, Klein medal 수상자의 수학교육이론 file 서울대 수학교육과 권오남
Math Colloquia A modified separation method to solve a heat-transfer boundary value problem file 서울대 경제학부 최병선
Math Colloquia Volume entropy of hyperbolic buildings file 서울대 임선희
Math Colloquia Contact Homology and Constructions of Contact Manifolds file 서울대 Otto van Koert
Math Colloquia Geometry, algebra and computation in moduli theory file 서울대 현동훈
Math Colloquia 정년퇴임 기념강연: 회고 file 서울대 김도한
Math Colloquia Weyl character formula and Kac-Wakimoto conjecture file 서울대 권재훈
Math Colloquia <학부생을 위한 ε 강연> 압축센싱과 행렬완성 file 서울대 심병효
Math Colloquia Theory and applications of partial differential equations file 서울대 변순식
Math Colloquia <학부생을 위한 ε 강연> 동형암호와 근사정수론 file 서울대 천정희
Math Colloquia An introduction to hyperplane arrangements file 서울대 이승진
Math Colloquia Periodic orbits in symplectic geometry file 서울대 강정수
Math Colloquia Mixing time of random processes file 서울대 서인석
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 Next
/ 11