# 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.

 제목+내용제목내용댓글이름닉네임태그
1. Green’s function for initial-boundary value problem

2. 16Apr
by 김수현
in 수학강연회

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

3. On the distributions of partition ranks and cranks

4. Q-curvature in conformal geometry

5. Zeros of the derivatives of the Riemann zeta function

6. Geometry, algebra and computation in moduli theory

7. Gromov-Witten-Floer theory and Lagrangian intersections in symplectic topology

8. High dimensional nonlinear dynamics

9. What is model theory?

10. Essential dimension of simple algebras

11. Restriction theorems for real and complex curves

12. Recommendation system and matrix completion: SVD and its applications (학부생을 위한 강연)

13. Deformation spaces of Kleinian groups and beyond

14. Idempotents and topologies

15. Recent progress on the Brascamp-Lieb inequality and applications

16. Existence of positive solutions for φ-Laplacian systems

17. Riemann-Hilbert correspondence for irregular holonomic D-modules

18. Normal form reduction for unconditional well-posedness of canonical dispersive equations

19. Random conformal geometry of Coulomb gas formalism

20. Categorification of Donaldson-Thomas invariants

Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 Next
/ 11