# Mechanization of proof: from 4-Color theorem to compiler verification

Extra Form
강연자 허충길
소속 서울대 컴퓨터공학부
date 2015-04-15

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.

 제목+내용제목내용댓글이름닉네임태그
List of Articles
카테고리 제목 소속 강연자
수학강연회 On some nonlinear elliptic problems Paul Sabatier University, Toulouse Yuri Egorov
수학강연회 On Ingram’s Conjecture University of Zagrab Sonja Stimac
수학강연회 On function field and smooth specialization of a hypersurface in the projective space KAIST 이용남
수학강연회 On circle diffeomorphism groups 고등과학원 김상현
수학강연회 Number theoretic results in a family Univ. of Toronto / KIAS Kim, Henry
수학강연회 Normal form reduction for unconditional well-posedness of canonical dispersive equations KAIST 권순식
수학강연회 Nonlocal generators of jump type Markov processes University of Bielefeld Walter Hoh
수학강연회 Noncommutative Surfaces 서강대학교 Jens Hoppe
수학강연회 Noncommutative Geometry. Quantum Space-Time and Diffeomorphism Invariant Geometry 서울대학교 Raphael Ponge
수학강연회 Non-commutative Lp-spaces and analysis on quantum spaces 서울대학교 이훈희
수학강연회 Noise-induced phenomena in stochastic heat equations 포항공대 김건우
수학강연회 Mixing time of random processes 서울대 서인석
수학강연회 Mixed type PDEs and compressible flow POSTECH 배명진
수학강연회 Mirror symmetry of pairings 숭실대학교 이상욱
수학강연회 Mechanization of proof: from 4-Color theorem to compiler verification 서울대 컴퓨터공학부 허충길
Maximal averages in harmonic analysis 서울대학교 이상혁
수학강연회 Mathematics, Biology and Mathematical Biology 부산대학교 수학과 정일효
수학강연회 Mathematical Models and Intervention Strategies for Emerging Infectious Diseases: MERS, Ebola and 2009 A/H1N1 Influenza 건국대학교 교수, 현 산업응용수학회 회장 정은옥
특별강연 Mathematical Analysis Models and Siumlations Collège de France Pierre-Louis Lions
수학강연회 Mathemaics & Hedge Fund 지큐자산운용 김택근
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Next
/ 15