Video

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

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.

 Subject+ContentSubjectContentCommentUser NameNick NameUser IDTag
1. ### Brownian motion and energy minimizing measure in negative curvature

..
CategoryMath Colloquia Dept.서울대학교 Lecturer임선희
2. ### 학부생을위한ε강연: 수학자는 왜 선망되는 직업일까?

현대 사회에서 수학의 역할과 수학자에 대한 수요는 갈수록 증가하고 있다. 미국의 어떤 조사에서는 수학자가 가장 선망 받는 직업으로 분류되고, 영국에서 수학이 경제에 미치는 영향을 분석한 Deloitte 보고서에 따르면 영국 직업의 10%가 수학 연구와 직접...
CategoryMath Colloquia Dept.KAIST Lecturer김동수
3. ### Generalized multiscale HDG (hybridizable discontinuous Galerkin) methods for flows in highly heterogeneous porous media

..
CategoryMath Colloquia Dept.육군사관학교 Lecturer문미남
4. ### Weyl character formula and Kac-Wakimoto conjecture

The character of the finite-dimensional irreducible modules over a finite-dimensional simple Lie algebra is given by the celebrated Weyl character formula. However, such a formula does not hold in general for finite-dimensional irreducible m...
CategoryMath Colloquia Dept.서울대 Lecturer권재훈
5. ### Nonlocal generators of jump type Markov processes

Empirical observations have shown that for an adequate description of many random phenomena non-Gaussian processes are needed. The paths of these Markov processes necessarily have jumps. Their generators are nonlocal operators which admit a ...
CategoryMath Colloquia Dept.University of Bielefeld LecturerWalter Hoh
6. ### 정년퇴임 기념강연: 회고

정년퇴임기념강연
CategoryMath Colloquia Dept.서울대 Lecturer김도한
7. ### <학부생을 위한 강연> 사색 정리를 포함하는 Hadwiger의 추측의 변형에 관하여

..
CategoryMath Colloquia Dept.KAIST Lecturer엄상일
8. ### The classification of fusion categories and operator algebras

..
CategoryMath Colloquia Dept.Kyoto University LecturerMasaki Izumi
9. ### Green’s function for initial-boundary value problem

In this talk, we will present an approach to construct the Green’s function for an initial boundary value problem with precise pointwise structure in the space-time domain. This approach is given in terms of transform variable and physical v...
CategoryMath Colloquia Dept.National Univ. of Singapore LecturerShih-Hsien Yu
10. ### 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 definit...
CategoryMath Colloquia Dept.서울대 컴퓨터공학부 Lecturer허충길
11. ### On the distributions of partition ranks and cranks

To explain Ramanujan's integer partition function congruences, Dyson's rank and Andrews-Garvan's crank have been introduced. The generating functions for these two partition statistics are typical examples of mock Jacobi forms and Jacobi for...
CategoryMath Colloquia Dept.서울과학기술대학교 Lecturer김병찬
12. ### Q-curvature in conformal geometry

In this talk, I will talk about the definition Q-curvature and some of its properties. Then I will talk about the problem of prescribing Q-curvature, especially I will explain the ideas of studying the problem using flow approach.
CategoryMath Colloquia Dept.서강대 LecturerPak Tung Ho
13. ### Zeros of the derivatives of the Riemann zeta function

I will introduce behavior of the derivatives of the Riemann zeta function.
CategoryMath Colloquia Dept.연세대 Lecturer기하서
14. ### Geometry, algebra and computation in moduli theory

I will explain the basic concepts of moduli and how moduli spaces can be constructed in algebraic geometry. Exploring the moduli spaces and issues arising from their construction lead to interesting interplay of geometry, algebra and computa...
CategoryMath Colloquia Dept.서울대 Lecturer현동훈
15. ### Gromov-Witten-Floer theory and Lagrangian intersections in symplectic topology

Gromov introduced the analytic method of pseudoholomorphic curves into the study of symplectic topology in the mid 80's and then Floer broke the conformal symmetry of the equation by twisting the equation by Hamiltonian vector fields. We sur...
CategoryMath Colloquia Dept.IBS, 포항공과대학교 Lecturer오용근
16. ### High dimensional nonlinear dynamics

In this talk, I am trying to introduce “what is high dimensional chaos” and also my research works in this area.
CategoryMath Colloquia Dept.경북대학교 Lecturer도영해
17. ### What is model theory?

I will introduce the basic notions of model theory, a branch of mathematical logic, and survey its applications to other areas of mathematics such as analysis, algebra, combinatorics and number theory. If time permits I will present recent w...
CategoryMath Colloquia Dept.연세대 Lecturer김병한
18. ### Essential dimension of simple algebras

The notion of essential dimension was introduced by Buhler and Reichstein in the late 90s. Roughly speaking, the essential dimension of an algebraic object is the minimal number of algebraically independent parameters one needs to define the...
CategoryMath Colloquia Dept.KAIST Lecturer백상훈