Stop when you are almost full: adventures in constructive termination
Dimitrios Vytiniotis
Thursday, 29 November 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Disjunctive well-foundedness, size-change termination, and well-quasi-orders are examples of techniques that have been successfully applied to program termination. Although these works originate in different communities, they rely on closely related principles and both employ similar arguments from Ramsey theory. At the same time there is a notable absence of these techniques in programming systems based on constructive type theory. In this talk, I will highlight the aforementioned connection and present a new toolkit for induction. Inevitably, this work has used some Ramsey-like arguments: Though similar proofs are typically classical, I will show an entirely constructive development that simplifies previous work of Bezem and Veldman.
(Joint work with Thierry Coquand and David Wahlstedt.)
Tarmo Uustalu
Last update 21.11.2012