https://www.math.snu.ac.kr/board/files/attach/images/701/ff97c54e6e21a4ae39315f9a12b27314.png
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.



Atachment
첨부 '1'
  1. High dimensional nonlinear dynamics

  2. Homogeneous dynamics and its application to number theory

  3. How to solve linear systems in practice

  4. Hybrid discontinuous Galerkin methods in computational science and engineering

  5. Idempotents and topologies

  6. Ill-posedness for incompressible Euler equations at critical regularit

  7. Infinite order rationally slice knots

  8. Integer partitions, q-series, and Modular forms

  9. Introduction to Non-Positively Curved Groups

  10. It all started with Moser

  11. Iwahori-Hecke algebras and beyond

  12. Iwasawa main conjecture and p-adic L-functions

  13. L-function: complex vs. p-adic

  14. Lie group actions on symplectic manifolds

  15. Limit computations in algebraic geometry and their complexity

  16. Mathemaics & Hedge Fund

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

  18. Mathematics, Biology and Mathematical Biology

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

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

  20. Mirror symmetry of pairings

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