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. Partial differential equations with applications to biology

    Partial differential equations with applications to biology
    Category수학강연회 소속POSTECH 강연자황형주
    Read More
  2. Diophantine equations and moduli spaces with nonlinear symmetry

    A fundamental result in number theory is that, under certain linear actions of arithmetic groups on homogeneous varieties, the integral points of the varieties decompose into finitely many orbits. For a classical example, the set of integra...
    Category수학강연회 소속서울대학교 강연자황준호
    Read More
  3. Symplectic Geometry, Mirror symmetry and Holomorphic Curves

    Symplectic geometry arose from the study of classical mechanics, and later many interesting symplectic invariants has been found since Gromov introduced techniques of J-holomorphic curves. Miraculously, such invariants are closely related wi...
    Category수학강연회 소속연세대 수학과 강연자홍한솔
    Read More
  4. Toward bridging a connection between machine learning and applied mathematics

    This lecture explores the topics and areas that have guided my research in computational mathematics and deep learning in recent years. Numerical methods in computational science are essential for comprehending real-world phenomena, and dee...
    Category수학강연회 소속성균관대학교 강연자홍영준
    Read More
  5. 돈은 어떻게 우리 삶에 돈며들었는가? (불확실성 시대에 부는 선형적으로 증가하는가?)

    1. 금본위제, 달러, 비트코인 등 돈의 흐름으로 보는 세계사 2. 사람은 어떻게 생각하고 행동하는가 ? (행동경제학, 비선형성) 3. 돈에 대한 생각, 행동, 습관을 바꾸어보자. (부자들은 무엇이 다른가 ? 지금부터 준비해보자.) 4. 주식, 부동산 등 자산관리 [...
    Category수학강연회 소속농협은행 강연자홍순옥
    Read More
  6. <학부생을 위한 ɛ 강연> Self-Supervised Learning in Computer Vision

    In recent years, artificial intelligence has made remarkable progress in developing algorithms that can learn from vast amounts of carefully labeled data. This paradigm of supervised learning has made great success in training specialist mo...
    Category수학강연회 소속인하대학교 강연자현윤석
    Read More
  7. Limit computations in algebraic geometry and their complexity

    Given a one-parameter family of algebraic varieties, its point-wise limit is usually too small whereas its algebraic limit is usually too big. I will introduce a notion of meaningful geometric limit and explain how it can be effectively comp...
    Category수학강연회 소속POSTECH 강연자현동훈
    Read More
  8. 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
  9. <학부생을 위한 ɛ 강연> Geometry and algebra of computational complexity

    학부생을 위한 이 강연에서는 고전적 튜링 기계의 기본적 정의로부터 시작하여 • 튜링기계를 비롯한 다양한 컴퓨터 모델의 복잡도 개념; • 계산(불)가능성 – 특히 디오판틴 방정식의 알고리즘적 해결법 (힐버트의 10번째 문제); • Non-deterministic 튜링 기계...
    Category수학강연회 소속서울대학교 강연자현동훈
    Read More
  10. 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
  11. 젊은과학자상 수상기념강연: From particle to kinetic and hydrodynamic descriptions to flocking and synchronization

    In this talk, I will report a recent progress for the modeling of collective behaviors of complex systems, in particular ocking and synchronization. Flocking and synchro-nization are ubiquitous in our daily life, for example, ocking of birds...
    Category수학강연회 소속서울대학교 강연자하승열
    Read More
  12. One and Two dimensional Coulomb Systems

    Coulomb Gases are point processes consisting of particles whose pair interaction is governed by the Coulomb potential. There is also an external potential which confines the particles to a region. Wigner introduced this toy model for the Gi...
    Category수학강연회 소속카이스트 강연자폴정
    Read More
  13. Seeded Ising Model for Human Iris Templates and Secure Distributed Iris Recognition

    Category수학강연회 소속서울대학교 강연자최형인
    Read More
  14. 극소곡면의 등주부등식

    둘레가 같은 평면의 영역중에서 넓이가 최대인 것은 원이라는 것이 등주부등식이다. 이와 똑 같은 등주부등식이 극소곡면에 대해서도 성립할 것이라는 예상이 90년 전에 제기되었다. 이 예상의 역사와 현주소에 대해서 알아보기로 하자.
    Category수학강연회 소속KIAS 강연자최재경
    Read More
  15. 원의 유리매개화에 관련된 수학

    The spaces admitting a rational parameterization are called rational. In particular plane conics, including circles, are rational. We will explain a few interesting applications of the rational parameterization of a circle. Also several exam...
    Category수학강연회 소속건국대학교 강연자최인송
    Read More
  16. 학부생을 위한 ε 강연회: Constructions by ruler and compass together with a conic

    Trisection of an angle and duplication of a cube are among the famous problems of Greeks. Although they were proven later to be impossible in general, Greeks already knew that one can trisect an angle and duplicate a cube by supplimenting se...
    Category수학강연회 소속건국대/서울대 강연자최인송
    Read More
  17. An equivalent condition to Bohr's for Dirichlet series

    초록: SNU-abstract.pdf
    Category수학강연회 소속포항공대 강연자최윤성
    Read More
  18. Birational Geometry of varieties with effective anti-canonical divisors

    Fano varieties are fundamental objects in algebraic geometry. These can be considered as the unique output of the -K -minimal model program on the varieties with effective anticanonical divisors. Thus the initial models should encode the in...
    Category수학강연회 소속연세대학교 강연자최성락
    Read More
  19. Fermat´s last theorem

    Fermat´s last theorem
    Category수학강연회 소속카이스트 강연자최서현
    Read More
  20. A modified separation method to solve a heat-transfer boundary value problem

    We derive a general solution of the heat equation through two modied separation methods. The obtained solution is expressed as linearly combined kernel solutions in terms of Hermite polynomials, which appears to provide an explanation of non...
    Category수학강연회 소속서울대 경제학부 강연자최병선
    Read More
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 Next
/ 12