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'
List of Articles
카테고리 제목 소속 강연자
수학강연회 <학부생을 위한 ε 강연> 압축센싱과 행렬완성 file 서울대 심병효
수학강연회 <학부생을 위한 ε 강연> 수학과 예술 - 초기 컴퓨터 그래픽 file 동양대학교 진중권
수학강연회 Faithful representations of Chevalley groups over quotient rings of non-Archimedean local fields file Univ. Bremen Keivan Mallahi-Karai
수학강연회 Quasi-homomorphisms into non-commutative groups file Kyoto Univ. Koji Fujiwara
수학강연회 Entropies on covers of compact manifolds file CNRS (France) François Ledrappier
수학강연회 Iwahori-Hecke algebras and beyond file University of Picardie Jules-Verne, Amiens 김성순
수학강연회 On the resolution of the Gibbs phenomenon file SUNY Buffalo 정재훈
수학강연회 <학부생을 위한 ε 강연> What mathematics can do for the real and even fake world file UCLA Stanley Osher
수학강연회 The process of mathematical modelling for complex and stochastic biological systems file KAIST 김재경
수학강연회 Random walks in spaces of negative curvature file Yale Univ. Giulio Tiozzo
수학강연회 Solver friendly finite element methods file Oklahoma State Univ. 구자언
수학강연회 Brownian motion and energy minimizing measure in negative curvature file 서울대학교 임선희
수학강연회 학부생을위한ε강연: 수학자는 왜 선망되는 직업일까? file KAIST 김동수
수학강연회 Generalized multiscale HDG (hybridizable discontinuous Galerkin) methods for flows in highly heterogeneous porous media file 육군사관학교 문미남
수학강연회 Weyl character formula and Kac-Wakimoto conjecture file 서울대 권재훈
수학강연회 Nonlocal generators of jump type Markov processes file University of Bielefeld Walter Hoh
특별강연 Regularity of solutions of Hamilton-Jacobi equation on a domain file ENS-Lyon Albert Fathi
특별강연 What is Weak KAM Theory? file ENS-Lyon Albert Fathi
수학강연회 정년퇴임 기념강연: 회고 file 서울대 김도한
수학강연회 <학부생을 위한 강연> 사색 정리를 포함하는 Hadwiger의 추측의 변형에 관하여 file KAIST 엄상일
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 13 Next
/ 13