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. 29Apr
    by 김수현
    in 수학강연회

    Geometric Langlands theory: A bridge between number theory and physics

  2. 13May
    by 김수현
    in 수학강연회

    <2020년도 젊은 과학자상 수상 기념강연> Metastability of stochastic systems

  3. 05Jun
    by 김수현
    in 수학강연회

    <정년퇴임 기념강연> 작용소대수와 양자정보이론

  4. 20Mar
    by 김수현
    in 수학강연회

    From mirror symmetry to enumerative geometry

  5. 17Oct
    by 김수현
    in 수학강연회

    <정년퇴임 기념강연> The Elements of Euclid

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

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

  7. 23Nov
    by 김수현
    in 수학강연회

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

  8. 20Oct
    by 김수현
    in 수학강연회

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

  9. 07Nov
    by Editor
    in 수학강연회

    Freudenthal medal, Klein medal 수상자의 수학교육이론

  10. 25Mar
    by 김수현
    in 수학강연회

    A modified separation method to solve a heat-transfer boundary value problem

  11. 01Nov
    by Manager
    in 수학강연회

    Volume entropy of hyperbolic buildings

  12. 01Nov
    by Manager
    in 수학강연회

    Contact Homology and Constructions of Contact Manifolds

  13. 16Mar
    by 김수현
    in 수학강연회

    Geometry, algebra and computation in moduli theory

  14. 09Jun
    by 김수현
    in 수학강연회

    정년퇴임 기념강연: 회고

  15. 22Sep
    by 김수현
    in 수학강연회

    Weyl character formula and Kac-Wakimoto conjecture

  16. 13Jun
    by 김수현
    in 수학강연회

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

  17. 12Sep
    by 김수현
    in 수학강연회

    Theory and applications of partial differential equations

  18. 17Oct
    by 김수현
    in 수학강연회

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

  19. 17Mar
    by 김수현
    in 수학강연회

    An introduction to hyperplane arrangements

  20. 08Sep
    by 김수현
    in 수학강연회

    Periodic orbits in symplectic geometry

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