https://www.math.snu.ac.kr/board/files/attach/images/701/ff97c54e6e21a4ae39315f9a12b27314.png
Extra Form
Lecturer 허충길
Dept. 서울대 컴퓨터공학부
date Apr 15, 2015

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
Attachment '1'
List of Articles
Category Subject Dept. Lecturer
Math Colloquia Partial differential equations with applications to biology file POSTECH 황형주
Math Colloquia Diophantine equations and moduli spaces with nonlinear symmetry file 서울대학교 황준호
Math Colloquia Symplectic Geometry, Mirror symmetry and Holomorphic Curves file 연세대 수학과 홍한솔
Math Colloquia Toward bridging a connection between machine learning and applied mathematics file 성균관대학교 홍영준
Math Colloquia 돈은 어떻게 우리 삶에 돈며들었는가? (불확실성 시대에 부는 선형적으로 증가하는가?) file 농협은행 홍순옥
Math Colloquia <학부생을 위한 ɛ 강연> Self-Supervised Learning in Computer Vision file 인하대학교 현윤석
Math Colloquia Limit computations in algebraic geometry and their complexity file POSTECH 현동훈
Math Colloquia Geometry, algebra and computation in moduli theory file 서울대 현동훈
Math Colloquia <학부생을 위한 ɛ 강연> Geometry and algebra of computational complexity file 서울대학교 현동훈
Math Colloquia Mechanization of proof: from 4-Color theorem to compiler verification file 서울대 컴퓨터공학부 허충길
Math Colloquia 젊은과학자상 수상기념강연: From particle to kinetic and hydrodynamic descriptions to flocking and synchronization file 서울대학교 하승열
Math Colloquia One and Two dimensional Coulomb Systems file 카이스트 폴정
Math Colloquia Seeded Ising Model for Human Iris Templates and Secure Distributed Iris Recognition file 서울대학교 최형인
Math Colloquia 극소곡면의 등주부등식 file KIAS 최재경
Math Colloquia 원의 유리매개화에 관련된 수학 file 건국대학교 최인송
Math Colloquia 학부생을 위한 ε 강연회: Constructions by ruler and compass together with a conic file 건국대/서울대 최인송
Math Colloquia An equivalent condition to Bohr's for Dirichlet series file 포항공대 최윤성
Math Colloquia Birational Geometry of varieties with effective anti-canonical divisors file 연세대학교 최성락
Math Colloquia Fermat´s last theorem file 카이스트 최서현
Math Colloquia A modified separation method to solve a heat-transfer boundary value problem file 서울대 경제학부 최병선
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 Next
/ 12