Thursday 20 September 2018, 14:00, LSV library: Termination checking using well-founded typing derivations, Rodolphe Lepigre (Deducteam).
Checking the termination of programs is a very difficult and important problem in contexts where consistency is critical (e.g., in proof assistants). One way of ensuring termination is to rely on well-known, Ramsay-based techniques such as the size change principle of Lee, Jones and Ben Amram. They roughly consist in analysing the recursive calls throughout programs, to ensure that there is some structural decrease (usually based on the subterm order). In this talk, I will present a new technique based on circular typing derivations, in which we rather analyse the “call structure” of circular typing derivations (also using a variant of the size change principle).
This is joint work with Christophe Raffalli.
Links: