BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Stop when you are Almost-Full: Adventures in Constructive Terminat
 ion - Dimitrios Vytiniotis
DTSTART:20111121T124500Z
DTEND:20111121T140000Z
UID:TALK33919@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Disjunctive well-foundedness (used in Terminator)\, size-chang
 e termination\, and well-quasi-orders (used in supercompilation and\nterm-
 rewrite systems) are examples of techniques that have been successfully ap
 plied to automatic proofs of program termination\nand online termination t
 esting\, respectively. Although these works originate in different communi
 ties\, there is an intimate connection\nbetween them - they rely on closel
 y related principles and both employ similar arguments from Ramsey theory.
  At the same time\nthere is a notable absence of these techniques in progr
 amming systems based on constructive type theory. In this paper we'd like 
 to\nhighlight the aforementioned connection and make the core ideas widely
  accessible to theoreticians and Coq programmers\, by offering\na Coq deve
 lopment which culminates in some novel tools for performing induction. The
  benefit is nice composability properties\nof termination arguments at the
  cost of natural user obligations which do not involve accessibility predi
 cates. Inevitably\,  we have to\npresent some Ramsey-like arguments: Thoug
 h similar proofs are typically classical\, we offer an entirely constructi
 ve development\nstanding on the shoulders of Veldman and Bezem\, and Richm
 an and Stolzenberg.\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR