Bogdan Vernescu (Worcester Polytechnic Institute) | 2015-04-03 14:00-15:30 |수학원리응용센터 중형세미나실
Considered one of the most important innovations in graduate science education in recent years, and the MBA of the 21st century, the Professional Science Master's (PSM) programs are a positive example of alignment of the higher education STEM production with the workforce demands. The fast growing number of PSM programs (331 PSM programs in 157 institutions in the United States) proves that the need to redesign the Master’s degree, to provide students with the skills needed to make them successful in jobs outside academia, responds to market needs for specialists with strong quantitative, modeling and scientific skills and that universities across the US have understood how to develop and deliver these programs.The PSM programs in the mathematical sciences have deeper roots in the applied mathematics and statistics MS programs and can be integrated well with the undergraduate and Ph.D. programs. There is evidence that shows that the programs meet the workforce needs and that graduates from these programs are successfully employed in corporations and in government.The talk will address several topics related to the development and administration of PSM programs in the mathematical sciences, such as:
허충길 교수 (서울대학교 컴퓨터공학부 소프트웨어이론 연구실) | 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.