http://web.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'
List of Articles
카테고리 제목 소속 강연자
수학강연회 <2020년도 젊은 과학자상 수상 기념강연> Metastability of stochastic systems file 서울대학교 서인석
수학강연회 <정년퇴임 기념강연> Hardy, Beurling, and invariant subspaces file 서울대학교 이우영
수학강연회 <정년퇴임 기념강연> The Elements of Euclid file 서울대/광주과학기술원 김홍종
수학강연회 <정년퇴임 기념강연> 리만 가설에 관련된 옌센 다항식의 영점 file 서울대학교 김영원
수학강연회 <정년퇴임 기념강연> 수학의 시대정신(?) file 서울대학교 수리과학부 김명환
수학강연회 <정년퇴임 기념강연> 작용소대수와 양자정보이론 file 서울대학교 계승혁
수학강연회 <청암상 수상 기념 특별강연> 동형암호, 기계학습, 근사정수론 file 서울대학교 수리과학부 천정희
수학강연회 <학부생을 위한 ɛ 강연> 196884=196883+1 file 이화여대 김현규
수학강연회 <학부생을 위한 ɛ 강연> 4차 산업혁명, 글로벌 디지털 혁신과 일자리 전쟁, 대학의 역할 file 서울대 전기정보공학부, 빅데이터연구원 원장 차상균
수학강연회 <학부생을 위한 ɛ 강연> A mathematical approach to xEV battery system file LG화학 안형준
수학강연회 <학부생을 위한 ɛ 강연> Continuous-time Portfolio Selection file 아주대학교 금융공학과 구형건
수학강연회 <학부생을 위한 ɛ 강연> Convergence of Fourier series and integrals in Lebesgue spaces file 서울대 이상혁
수학강연회 <학부생을 위한 ɛ 강연> Geometry and algebra of computational complexity file 서울대학교 현동훈
수학강연회 <학부생을 위한 ɛ 강연> Introduction to the incompressible Navier-Stokes equations file UNIST 배한택
수학강연회 <학부생을 위한 ɛ 강연> Intuition, Mathematics and Proof file KAIST 수리과학과 김동수
수학강연회 <학부생을 위한 ɛ 강연> Mathematical Aspects of Machine Learning and Deep Learning AI file 서울대학교 컴퓨터공학부 장병탁
수학강연회 <학부생을 위한 ɛ 강연> Mathematics and music: Pythagoras, Bach, Fibonacci and AI file 피아니스트 임현정
수학강연회 <학부생을 위한 ɛ 강연> Secure computation: Promise and challenges file 송용수 <학부생을 위한 ɛ 강연> Secure computation: Promise and challenges
수학강연회 <학부생을 위한 ɛ 강연> Self-Supervised Learning in Computer Vision file 인하대학교 현윤석
수학강연회 <학부생을 위한 ɛ 강연> Symplectic geometry and the three-body problem file 서울대학교 Otto van Koert
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 Next
/ 12