The National Center for Supercomputing Applications (NCSA) is hosting its monthly colloquium series and invites everyone to participate in the September session.
This month's event will be led by Kohei Kishida, Associate Professor of Philosophy at the University of Illinois. He is also affiliated with Mathematics and Computer Science, and is a member of the Illinois Quantum Information Science and Technology Center (IQUIST). His research centers on logic, category theory, and their applications to computer science and quantum foundations.He will present "Quantum Programming Languages with Types and Semantics".
Quantum programming plays an essential role in making quantum computing practical and scalable. One of its current challenges is to provide quantum programming languages with formal methods, which are all the more essential due to non-classical properties of quantum physics. In this talk, I will first lay out what purposes quantum programming languages are expected to serve, why these objectives call for formal methods, and why features such as dependent types are highly desirable. I will then discuss my recent work that achieved several of such features: e.g., one of the languages I developed was the first quantum programming language to have a linear dependent type theory and denotational semantics. As will become clear, insights from research in quantum foundations help us devise formal methods in quantum computing and programming.