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. The process of mathematical modelling for complex and stochastic biological systems

    The revolution of molecular biology in the early 1980s has revealed complex network of non-linear and stochastic biochemical interactions underlying biological systems. To understand this complex system, mathematical models have been widely ...
    Category수학강연회 소속KAIST 강연자김재경
    Read More
  2. Random walks in spaces of negative curvature

    Given a group of isometries of a metric space, one can draw a random sequence of group elements, and look at its action on the space.  What are the asymptotic properties of such a random walk?  The answer depends on the geometry of the space...
    Category수학강연회 소속Yale Univ. 강연자Giulio Tiozzo
    Read More
  3. Solver friendly finite element methods

    In this talk, numerical methods to solve second-order elliptic partial dierential equations will be presented. First, some of the existing methods, such as the standard Galerkin method, mixed nite element methods etc., will be briey discusse...
    Category수학강연회 소속Oklahoma State Univ. 강연자구자언
    Read More
  4. Brownian motion and energy minimizing measure in negative curvature

    ..
    Category수학강연회 소속서울대학교 강연자임선희
    Read More
  5. 학부생을위한ε강연: 수학자는 왜 선망되는 직업일까?

    현대 사회에서 수학의 역할과 수학자에 대한 수요는 갈수록 증가하고 있다. 미국의 어떤 조사에서는 수학자가 가장 선망 받는 직업으로 분류되고, 영국에서 수학이 경제에 미치는 영향을 분석한 Deloitte 보고서에 따르면 영국 직업의 10%가 수학 연구와 직접...
    Category수학강연회 소속KAIST 강연자김동수
    Read More
  6. Generalized multiscale HDG (hybridizable discontinuous Galerkin) methods for flows in highly heterogeneous porous media

    ..
    Category수학강연회 소속육군사관학교 강연자문미남
    Read More
  7. Weyl character formula and Kac-Wakimoto conjecture

    The character of the finite-dimensional irreducible modules over a finite-dimensional simple Lie algebra is given by the celebrated Weyl character formula. However, such a formula does not hold in general for finite-dimensional irreducible m...
    Category수학강연회 소속서울대 강연자권재훈
    Read More
  8. Nonlocal generators of jump type Markov processes

    Empirical observations have shown that for an adequate description of many random phenomena non-Gaussian processes are needed. The paths of these Markov processes necessarily have jumps. Their generators are nonlocal operators which admit a ...
    Category수학강연회 소속University of Bielefeld 강연자Walter Hoh
    Read More
  9. Regularity of solutions of Hamilton-Jacobi equation on a domain

    150902_HYKE.pdf
    Category특별강연 소속ENS-Lyon 강연자Albert Fathi
    Read More
  10. What is Weak KAM Theory?

    The goal of this lecture is to explain and motivate the connection between AubryMather theory (Dynamical Systems), and viscosity solutions of the Hamilton-Jacobi equation (PDE). This connection is the content of weak KAM Theory. The talk sho...
    Category특별강연 소속ENS-Lyon 강연자Albert Fathi
    Read More
  11. 정년퇴임 기념강연: 회고

    정년퇴임기념강연
    Category수학강연회 소속서울대 강연자김도한
    Read More
  12. <학부생을 위한 강연> 사색 정리를 포함하는 Hadwiger의 추측의 변형에 관하여

    ..
    Category수학강연회 소속KAIST 강연자엄상일
    Read More
  13. The classification of fusion categories and operator algebras

    ..
    Category수학강연회 소속Kyoto University 강연자Masaki Izumi
    Read More
  14. Green’s function for initial-boundary value problem

    In this talk, we will present an approach to construct the Green’s function for an initial boundary value problem with precise pointwise structure in the space-time domain. This approach is given in terms of transform variable and physical v...
    Category수학강연회 소속National Univ. of Singapore 강연자Shih-Hsien Yu
    Read More
  15. Mechanization of proof: from 4-Color theorem to compiler verification

    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 definit...
    Category수학강연회 소속서울대 컴퓨터공학부 강연자허충길
    Read More
  16. On the distributions of partition ranks and cranks

    To explain Ramanujan's integer partition function congruences, Dyson's rank and Andrews-Garvan's crank have been introduced. The generating functions for these two partition statistics are typical examples of mock Jacobi forms and Jacobi for...
    Category수학강연회 소속서울과학기술대학교 강연자김병찬
    Read More
  17. Q-curvature in conformal geometry

    In this talk, I will talk about the definition Q-curvature and some of its properties. Then I will talk about the problem of prescribing Q-curvature, especially I will explain the ideas of studying the problem using flow approach.
    Category수학강연회 소속서강대 강연자Pak Tung Ho
    Read More
  18. Zeros of the derivatives of the Riemann zeta function

    I will introduce behavior of the derivatives of the Riemann zeta function.
    Category수학강연회 소속연세대 강연자기하서
    Read More
  19. Geometry, algebra and computation in moduli theory

    I will explain the basic concepts of moduli and how moduli spaces can be constructed in algebraic geometry. Exploring the moduli spaces and issues arising from their construction lead to interesting interplay of geometry, algebra and computa...
    Category수학강연회 소속서울대 강연자현동훈
    Read More
  20. Gromov-Witten-Floer theory and Lagrangian intersections in symplectic topology

    Gromov introduced the analytic method of pseudoholomorphic curves into the study of symplectic topology in the mid 80's and then Floer broke the conformal symmetry of the equation by twisting the equation by Hamiltonian vector fields. We sur...
    Category수학강연회 소속IBS, 포항공과대학교 강연자오용근
    Read More
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 Next
/ 16