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.

Attachment '1'
List of Articles
Category Subject Dept. Lecturer
Math Colloquia <학부생을 위한 ɛ 강연> Secure computation: Promise and challenges file 송용수 <학부생을 위한 ɛ 강연> Secure computation: Promise and challenges
Special Colloquia Regularity of solutions of Hamilton-Jacobi equation on a domain file ENS-Lyon Albert Fathi
Special Colloquia What is Weak KAM Theory? file ENS-Lyon Albert Fathi
Math Colloquia Fano manifolds of Calabi-Yau Type file 서울대학교 Atanas Iliev
Math Colloquia Sums of squares in quadratic number rings file Univ. of Kentucky David Leep
Special Colloquia Queer Lie Superalgebras file Univ. of Texas, Arlington Dimitar Grantcharov
Math Colloquia Entropies on covers of compact manifolds file CNRS (France) François Ledrappier
Math Colloquia Quantum Dynamics in the Mean-Field and Semiclassical Regime file Ecole Polytechnique Francoise Golse
Math Colloquia Random walks in spaces of negative curvature file Yale Univ. Giulio Tiozzo
Classification of simple amenable operator algebras file Lakehead University Grazia Viola
Special Colloquia Persistent Homology file Stanford University Gunnar E. Carlsson
Special Colloquia Structures on Persistence Barcodes and Generalized Persistence file Stanford University Gunnar E. Carlsson
Special Colloquia Topological Mapping of Point Cloud Data file Stanford University Gunnar E. Carlsson
Math Colloquia The Shape of Data file Stanford University Gunnar E. Carlsson
Math Colloquia The significance of dimensions in mathematics file Kyoto Univ./서울대학교 Heisuke Hironaka
Math Colloquia Topological aspects in the theory of aperiodic solids and tiling spaces file Georgia Institute of Technology, School of Mathematics and School of Physics Jean V. Bellissard
Math Colloquia Noncommutative Surfaces file 서강대학교 Jens Hoppe
BK21 FOUR Rookies Pitch 2022-1 Rookies Pitch: Harmonic Analysis (Kalachand Shuin) file BK21 Kalachand Shuin
Math Colloquia Conformal field theory and noncommutative geometry file 동경대학교 Kawahigashi
Math Colloquia Faithful representations of Chevalley groups over quotient rings of non-Archimedean local fields file Univ. Bremen Keivan Mallahi-Karai
Board Pagination Prev 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Next
/ 15