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'
  1. <학부생을 위한 ε 강연> Variable-driven sociological research with data innovations

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

  3. <학부생을 위한 ε 강연> 동형암호와 근사정수론

  4. 4-manifold topology and disk embedding

  5. Hybrid discontinuous Galerkin methods in computational science and engineering

  6. The phase retrieval problem

  7. Theory and applications of partial differential equations

  8. Analysis and computations of stochastic optimal control problems for stochastic PDEs

  9. <학부생을 위한 ε 강연> 압축센싱과 행렬완성

  10. <학부생을 위한 ε 강연> 수학과 예술 - 초기 컴퓨터 그래픽

  11. Faithful representations of Chevalley groups over quotient rings of non-Archimedean local fields

  12. Quasi-homomorphisms into non-commutative groups

  13. Entropies on covers of compact manifolds

  14. Iwahori-Hecke algebras and beyond

  15. On the resolution of the Gibbs phenomenon

  16. <학부생을 위한 ε 강연> What mathematics can do for the real and even fake world

  17. The process of mathematical modelling for complex and stochastic biological systems

  18. Random walks in spaces of negative curvature

  19. Solver friendly finite element methods

  20. Brownian motion and energy minimizing measure in negative curvature

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