https://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
카테고리 제목 소속 강연자
수학강연회 Partial differential equations with applications to biology file POSTECH 황형주
수학강연회 Diophantine equations and moduli spaces with nonlinear symmetry file 서울대학교 황준호
수학강연회 Symplectic Geometry, Mirror symmetry and Holomorphic Curves file 연세대 수학과 홍한솔
수학강연회 Toward bridging a connection between machine learning and applied mathematics file 성균관대학교 홍영준
수학강연회 돈은 어떻게 우리 삶에 돈며들었는가? (불확실성 시대에 부는 선형적으로 증가하는가?) file 농협은행 홍순옥
수학강연회 <학부생을 위한 ɛ 강연> Self-Supervised Learning in Computer Vision file 인하대학교 현윤석
수학강연회 Limit computations in algebraic geometry and their complexity file POSTECH 현동훈
수학강연회 Geometry, algebra and computation in moduli theory file 서울대 현동훈
수학강연회 <학부생을 위한 ɛ 강연> Geometry and algebra of computational complexity file 서울대학교 현동훈
BK21 FOUR Rookies Pitch 2022-2 Rookies Pitch: Representation Theory(허태혁) file QSMS 허태혁
수학강연회 Mechanization of proof: from 4-Color theorem to compiler verification file 서울대 컴퓨터공학부 허충길
특별강연 허준이 교수 호암상 수상 기념 강연 (Lorentzian Polynomials) file Professor, Stanford University 허준이 교수
특별강연 Combinatorics and Hodge theory file 미국 프린스턴대 교수, 한국 고등과학원 석학교수 허준이
BK21 FOUR Rookies Pitch 2022-2 Rookies Pitch: Harmonic Analysis (함세헌) file 수학연구소 함세헌
수학강연회 젊은과학자상 수상기념강연: From particle to kinetic and hydrodynamic descriptions to flocking and synchronization file 서울대학교 하승열
수학강연회 One and Two dimensional Coulomb Systems file 카이스트 폴정
수학강연회 Seeded Ising Model for Human Iris Templates and Secure Distributed Iris Recognition file 서울대학교 최형인
BK21 FOUR Rookies Pitch 2023-2 Generative Model(최재웅) file KIAS AI 기초과학센터 최재웅
수학강연회 극소곡면의 등주부등식 file KIAS 최재경
수학강연회 원의 유리매개화에 관련된 수학 file 건국대학교 최인송
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Next
/ 15