Event Detail

Fri Mar 20, 2015–Sat Mar 21, 2015
60 Evans Hall, 11 PM–1 AM
Logic Colloquium
Keita Yokoyama (Japan Advanced Institute of Science and Technology)
Reverse Mathematics and Program Termination

It is well-known that proof theory and computer science have a good connection. In this talk, I will focus on the relation between reverse mathematics and the study of program termination. In the study of reverse mathematics, Ramsey’s theorem is one of the most important topics and the strength of Ramsey’s theorem is well-investigated from both of the proof-theoretic view point and the computability theoretic view point. On the other hand, Ramsey’s theorem is often used in computer science. In the study of termination analysis, Podelski/Rybalchenko used Ramsey’s theorem for pairs to introduce a new algorithm for termination checking. Looking at the above connection with Ramsey’s theorem, we study the relation between reverse mathematics and termination analysis.

This is a joint work with Stefano Berardi and Silvia Steila.