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
카테고리 제목 소속 강연자
수학강연회 정년퇴임 기념강연회: 숙제 file 서울대학교 지동표
수학강연회 Classical and Quantum Probability Theory file 충북대학교 지운식
수학강연회 <학부생을 위한 ε 강연> 수학과 예술 - 초기 컴퓨터 그래픽 file 동양대학교 진중권
수학강연회 <학부생을 위한 ɛ 강연> 4차 산업혁명, 글로벌 디지털 혁신과 일자리 전쟁, 대학의 역할 file 서울대 전기정보공학부, 빅데이터연구원 원장 차상균
수학강연회 4-manifold topology and disk embedding file 포항공과대학교 차재춘
특별강연 A New Approach to Discrete Logarithm with Auxiliary Inputs file 서울대학교 천정희
수학강연회 <학부생을 위한 ε 강연> 동형암호와 근사정수론 file 서울대 천정희
수학강연회 <청암상 수상 기념 특별강연> 동형암호, 기계학습, 근사정수론 file 서울대학교 수리과학부 천정희
수학강연회 Topological surgery through singularity in mean curvature flow file 고등과학원 최경수
수학강연회 A modified separation method to solve a heat-transfer boundary value problem file 서울대 경제학부 최병선
수학강연회 Fermat´s last theorem file 카이스트 최서현
수학강연회 Birational Geometry of varieties with effective anti-canonical divisors file 연세대학교 최성락
BK21 FOUR Rookies Pitch 2021-1 Rookies Pitch: Representation Theory (최승일) file QSMS 최승일
수학강연회 An equivalent condition to Bohr's for Dirichlet series file 포항공대 최윤성
수학강연회 원의 유리매개화에 관련된 수학 file 건국대학교 최인송
수학강연회 학부생을 위한 ε 강연회: Constructions by ruler and compass together with a conic file 건국대/서울대 최인송
수학강연회 극소곡면의 등주부등식 file KIAS 최재경
BK21 FOUR Rookies Pitch 2023-2 Generative Model(최재웅) file KIAS AI 기초과학센터 최재웅
수학강연회 Seeded Ising Model for Human Iris Templates and Secure Distributed Iris Recognition file 서울대학교 최형인
수학강연회 One and Two dimensional Coulomb Systems file 카이스트 폴정
Board Pagination Prev 1 ... 4 5 6 7 8 9 10 11 12 13 14 15 Next
/ 15