University of Cambridge > > Semantics Lunch (Computer Laboratory) > Stop when you are Almost-Full: Adventures in Constructive Termination

Stop when you are Almost-Full: Adventures in Constructive Termination

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

Disjunctive well-foundedness (used in Terminator), size-change termination, and well-quasi-orders (used in supercompilation and term-rewrite systems) are examples of techniques that have been successfully applied to automatic proofs of program termination and online termination testing, respectively. Although these works originate in different communities, there is an intimate connection between them – 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 paper we’d like to highlight the aforementioned connection and make the core ideas widely accessible to theoreticians and Coq programmers, by offering a Coq development which culminates in some novel tools for performing induction. The benefit is nice composability properties of termination arguments at the cost of natural user obligations which do not involve accessibility predicates. Inevitably, we have to present some Ramsey-like arguments: Though similar proofs are typically classical, we offer an entirely constructive development standing on the shoulders of Veldman and Bezem, and Richman and Stolzenberg.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity