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

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. 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
2. 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수학강연회 소속서울대 컴퓨터공학부 강연자허충길
3. 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수학강연회 소속서울과학기술대학교 강연자김병찬
4. 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
5. Zeros of the derivatives of the Riemann zeta function

I will introduce behavior of the derivatives of the Riemann zeta function.
Category수학강연회 소속연세대 강연자기하서
6. 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수학강연회 소속서울대 강연자현동훈
7. 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, 포항공과대학교 강연자오용근
8. High dimensional nonlinear dynamics

In this talk, I am trying to introduce “what is high dimensional chaos” and also my research works in this area.
Category수학강연회 소속경북대학교 강연자도영해
9. What is model theory?

I will introduce the basic notions of model theory, a branch of mathematical logic, and survey its applications to other areas of mathematics such as analysis, algebra, combinatorics and number theory. If time permits I will present recent w...
Category수학강연회 소속연세대 강연자김병한
10. Essential dimension of simple algebras

The notion of essential dimension was introduced by Buhler and Reichstein in the late 90s. Roughly speaking, the essential dimension of an algebraic object is the minimal number of algebraically independent parameters one needs to define the...
Category수학강연회 소속KAIST 강연자백상훈
11. Restriction theorems for real and complex curves

We will talk about the Fourier restriction theorems for non-degenerate and degenerate curves in Euclidean space Rd. This problem was first studied by E. M. Stein and C. Fefferman for the circle and sphere, and it still remains an unsolved pr...
Category수학강연회 소속포항공과대학교 강연자박종국
12. Recommendation system and matrix completion: SVD and its applications (학부생을 위한 강연)

이 강연에서는 최근 음악, 영화 추천 등 다양한 Recommendation System의 기본 아이디어인 Matrix Completion 문제와, 이를 해결하기 위해 Singular Value Decomposition을 통한 차원 축소 및 내재 공간 학습이 어떤 원리로 이루어 지는지 설명합니다. 그리고 ...
Category수학강연회 소속서울대 전기공학부 강연자정교민
13. Deformation spaces of Kleinian groups and beyond

From 1980’s, the study of Kleinian groups has been carried out in the framework of the paradigm of “Thurston’s problems”. Now they are all solved, and we can tackle deeper problems; for instance to determine the topological types of the defo...
Category수학강연회 소속Osaka University 강연자Kenichi Ohshika
14. Idempotents and topologies

A classical theorem of Jacobs, de Leeuw and Glicksberg shows that a representation of a group on a reflexive Banach space may be decomposed into a returning subspace and a weakly mixing subspace. This may be realized as arising from the idem...
Category수학강연회 소속University of Waterloo 강연자Nico Spronk
15. Recent progress on the Brascamp-Lieb inequality and applications

In his survey paper in the Bulletin of the AMS from 2002, R. J. Gardner discussed the Brunn-Minkowski inequality, stating that it deserves to be better known and painted a beautiful picture of its relationship with other inequalities in anal...
Category수학강연회 소속Saitama University 강연자Neal Bez
16. Existence of positive solutions for φ-Laplacian systems

SNU-LeeAbstract.pdf
Category수학강연회 소속이용훈 강연자수학강연회,특별강연,대중강연
17. Riemann-Hilbert correspondence for irregular holonomic D-modules

The original Riemann-Hilbert problem is to construct a liner ordinary differential equation with regular singularities whose solutions have a given monodromy. Nowadays, it is formulated as a categorical equivalence of the category of regular...
Category수학강연회 소속서울대학교/RIMS 강연자Masaki Kashiwara
18. Normal form reduction for unconditional well-posedness of canonical dispersive equations

Normal form method is a classical ODE technique begun by H. Poincare. Via a suitable transformation one reduce a differential equation to a simpler form, where most of nonresonant terms are cancelled. In this talk, I begin to explain the not...
Category수학강연회 소속KAIST 강연자권순식