http://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'
List of Articles
카테고리 제목 소속 강연자
수학강연회 곡선의 정의란 무엇인가? file 서울대학교 김영훈
수학강연회 Categorification of Donaldson-Thomas invariants file 서울대학교 김영훈
BK21 FOUR Rookies Pitch 2021-2 Rookies Pitch: Representation Theory(김영훈) file QSMS 김영훈
수학강연회 <학부생을 위한 ɛ 강연> 양자상태의 기하학 file 고등과학원 김영훈
수학강연회 <정년퇴임 기념강연> 리만 가설에 관련된 옌센 다항식의 영점 file 서울대학교 김영원
BK21 FOUR Rookies Pitch 2022-2 Rookies Pitch: Geometric Topology (김승원) file 성균관대학교 김승원
수학강연회 On the Schauder theory for elliptic PDEs file 연세대학교 김세익
수학강연회 Iwahori-Hecke algebras and beyond file University of Picardie Jules-Verne, Amiens 김성순
수학강연회 Introduction to Non-Positively Curved Groups file KAIST 김상현
수학강연회 Subgroups of Mapping Class Groups file 서울대학교 김상현
수학강연회 On circle diffeomorphism groups file 고등과학원 김상현
수학강연회 What is model theory? file 연세대 김병한
수학강연회 Integer partitions, q-series, and Modular forms file 서울과학기술 대학 김병찬
수학강연회 On the distributions of partition ranks and cranks file 서울과학기술대학교 김병찬
수학강연회 Topology and number theory file Univ. College London/포항공대 김민형
BK21 FOUR Rookies Pitch 2023-1 Number Theory (김민규) file 성균관대학교 김민규
수학강연회 <정년퇴임 기념강연> 수학의 시대정신(?) file 서울대학교 수리과학부 김명환
BK21 FOUR Rookies Pitch 2023-1 Algebraic Combinatorics (김동현) file BK21 김동현
수학강연회 The Lagrange and Markov Spectra of Pythagorean triples file 동국대학교 김동한
수학강연회 Subword complexity, expansion of real numbers and irrationality exponents file 동국대 김동한
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Next
/ 15