Seminar
Mechanization of Proof: From 4-Color Theorem to Compiler Verification
허충길 교수 (서울대학교 컴퓨터공학부 소프트웨어이론 연구실)
|
2014-08-27 16:30~17:30
|수학원리응용센터 중형세미나실
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.
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.
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.
More
3월_NIMS 집중강연 및 콜로퀴움.pdf