# 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. Conformal field theory in mathematics

2. <학부생을 위한 ɛ 강연> A mathematical approach to xEV battery system

3. Anomalous diffusions and fractional order differential equations

4. Seeded Ising Model for Human Iris Templates and Secure Distributed Iris Recognition

5. <학부생을 위한 ɛ 강연> 4차 산업혁명, 글로벌 디지털 혁신과 일자리 전쟁, 대학의 역할

6. An equivalent condition to Bohr's for Dirichlet series

7. On the Schauder theory for elliptic PDEs

8. <학부생을 위한 ɛ 강연> 서비스 진보의 관점에서 본 AI technology

9. Seifert fiberings

10. Mixing time of random processes

11. Periodic orbits in symplectic geometry

12. <학부생을 위한 ɛ 강연> 196884=196883+1

13. Mathematical Models and Intervention Strategies for Emerging Infectious Diseases: MERS, Ebola and 2009 A/H1N1 Influenza

14. Convex and non-convex optimization methods in image processing

15. Creation of concepts for prediction models and quantitative trading

16. <학부생을 위한 ɛ 강연> Introduction to the incompressible Navier-Stokes equations

17. An introduction to hyperplane arrangements

18. What happens inside a black hole?

19. <학부생을 위한 ε 강연> Variable-driven sociological research with data innovations

20. Subword complexity, expansion of real numbers and irrationality exponents

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