Invitation seminar

Creating Tomorrow's Mathematics Professionals-PSM Programs in the Mathematical Sciences

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:
Curriculum issues: courses offered, how content is related to businesses' needs, special pedagogical issues related to teaching in a PSM, etc.
Internship and research components in the PSMs.
Building effective partnerships between math PSMs and industry, business and government.
Student recruitment and retention.
Role of the PSMs in creating leaders in innovative companies in STEM fields: case studies of working mathematicians.
Start-up strategies and costs for new PSMs.

Invitation 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.