공지사항
NIMS 초청세미나(서울대 허충길교수/14.8.27(목))
등록일자 : 2014-08-27
안녕하십니까.
국가수리과학연구소에서는 사회 각 분야별 이슈와 관련한 전문가 초청 세미나를 통해 전문지식 및 식견을 확대하고자,
아래와 같이 NIMS 초청세미나를 개최하고자 합니다.
많은 참석 부탁드립니다.
1. 연사 : 허충길 교수 (서울대학교 컴퓨터공학부 소프트웨어 이론 연구실)
2. 일시 : 2014년 8월 27일(수) 오후 4시 30분
3. 장소 : 국가수리과학연구소 수학원리응용센터 세미나실
4. 제목 : Mechanization of Proof: From 4-Color Theorem to Compiler Verification
5. 대상 : 관심있는 분은 누구나 참석 가능
Abstract
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.
국가수리과학연구소에서는 사회 각 분야별 이슈와 관련한 전문가 초청 세미나를 통해 전문지식 및 식견을 확대하고자,
아래와 같이 NIMS 초청세미나를 개최하고자 합니다.
많은 참석 부탁드립니다.
1. 연사 : 허충길 교수 (서울대학교 컴퓨터공학부 소프트웨어 이론 연구실)
2. 일시 : 2014년 8월 27일(수) 오후 4시 30분
3. 장소 : 국가수리과학연구소 수학원리응용센터 세미나실
4. 제목 : Mechanization of Proof: From 4-Color Theorem to Compiler Verification
5. 대상 : 관심있는 분은 누구나 참석 가능
Abstract
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.
안녕하십니까.
국가수리과학연구소에서는 사회 각 분야별 이슈와 관련한 전문가 초청 세미나를 통해 전문지식 및 식견을 확대하고자,
아래와 같이 NIMS 초청세미나를 개최하고자 합니다.
많은 참석 부탁드립니다.
1. 연사 : 허충길 교수 (서울대학교 컴퓨터공학부 소프트웨어 이론 연구실)
2. 일시 : 2014년 8월 27일(수) 오후 4시 30분
3. 장소 : 국가수리과학연구소 수학원리응용센터 세미나실
4. 제목 : Mechanization of Proof: From 4-Color Theorem to Compiler Verification
5. 대상 : 관심있는 분은 누구나 참석 가능
Abstract
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.
국가수리과학연구소에서는 사회 각 분야별 이슈와 관련한 전문가 초청 세미나를 통해 전문지식 및 식견을 확대하고자,
아래와 같이 NIMS 초청세미나를 개최하고자 합니다.
많은 참석 부탁드립니다.
1. 연사 : 허충길 교수 (서울대학교 컴퓨터공학부 소프트웨어 이론 연구실)
2. 일시 : 2014년 8월 27일(수) 오후 4시 30분
3. 장소 : 국가수리과학연구소 수학원리응용센터 세미나실
4. 제목 : Mechanization of Proof: From 4-Color Theorem to Compiler Verification
5. 대상 : 관심있는 분은 누구나 참석 가능
Abstract
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.
