Emanuele Frittaion
CMAF-CIO, Universidade de Lisboa

Abstract: In [2] the authors address the reverse mathematics of Podelski and Rybalchenko termination theorem for transition based program.
In a joint work with Silvia Steila, Keita Yokoyama, and Florian Pelupessy, we tackle the reverse mathematics of size-change termination (SCT), another tool in program analysis which supports automated termination proofs. Part of this work has been published in [1]. The project contributes to the reverse mathematics of termination analysis.
We discuss two aspects of SCT: the (1) SCT criterion and the (2) SCT soundness. (1)  gives a characterization of SCT that makes size-change termination suitable for automation. As usual, Ramsey's theorem for pairs turns out to play an essential role. (2) is simply the statement that "every SCT program terminates”. One of the motivations for studying (2) is that the (program for the) Peter-Ackermann function is easily (in fact provably in RCA0) seen to be SCT.

[1] Emanuele Frittaion, Silvia Steila and Keita Yokoyama. The strength of the SCT criterion. Preprint at https://arxiv.org/abs/1611.05176.
[2] Silvia Steila and Keita Yokoyama. Reverse mathematical bounds for the termination theorem. Annals of Pure Applied Logic, 167(12):1213–1241, 2016.

This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.