SMSS Colloquium Talk - Chris Kapulkin
Date:
Thursday, February 15, 2018
Time:
3:30 pm
Location:
North Campus Building (NCB)
Room: 114
Room: 114
Cost:
Free
Share:
Export:
Speaker: Chris Kapulkin (Western University, Math Department)
Title: Formal verification
Abstract: A formal proof is a proof that has been checked by a piece of computer software, called a proof assistant, down to the very first axioms of mathematics. Over the last 30 years, several sizable proofs were formalized and the use of proof assistants is now common in industry, to verify e.g. the correctness of cryptographic protocols, operating system kernels, and air traffic control systems. This talk will be an introduction to proof assistants, presenting the main mathematical ideas behind them, as well as the challenges ahead.
Contact:
Event Type:
Audience:
Department:
