Computer Assisted Theorem Proving and Applications

Reference No.	2024a024
Type/Category	Grant for Project Research-Short-term Joint Research
Title of Research Project	Computer Assisted Theorem Proving and Applications
Principal Investigator	Jacques Garrigue（Nagoya University Graduate School of Mathematics・Professor）
Research Period	November 25,2024. - November 26,2024.
Keyword(s) of Research Fields	Proof assistant, formal logic, type theory, higher-order logic, programming language theory, algorithmic, formal proof
Abstract for Research Report	(1) The needs for proofs are increasing in our society. Bugs in the implementation of algorithms that support many infrastructures can have costs in billions of yens, and even cost lives. They must also be correct mathematically. (2) Interactive proof assistants are designed to check that every step is correct in a proof. This approach works for both mathematical and software proofs, and is arguably the only way to guarantee full correctness. The need for human interaction in proof assistants comes from Turing's negation of the Entscheidungsproblem, meaning that a fully automatic theorem prover cannot prove all theorems. (3) This project aims at bringing together users and developers of proof assistants. By organizing a meeting, we hope to dynamize the field. We intend to bring people from various communities such as programming languages, algorithms, pure and applied mathematics. We do not restrict the kind of proof assistant used, and offer a forum to exchange ideas between them. (4) The domestic TPP workshop has been active in this field for many years. We intend to organize the 20th edition of TPP at Kyushu University, also inviting researchers from oversees.
Organizing Committee Members (Workshop) Participants (Short-term Joint Usage)	Jacques Garrigue（Nagoya University・Professor） Yasuhiko Minamide（Tokyo Institute of Technology・Professor） Kazuhisa Nakasho（Yamaguchi University・Associate Professor）