Personal tools
You are here: Home Events James Cheney: How not to prove termination

James Cheney: How not to prove termination

When Oct 30, 2012
from 01:00 PM to 02:00 PM
Where MF2
Add event to calendar vCal

The story you are about to hear is true; only the names have been changed to protect the innocent.  In this talk I'll present a proof of termination (strong normalization) of a rewriting system that has a subtle error.  However, the rewrite system does turn out to be (weakly) normalizing, provided the rules are applied according to a specific strategy.  The error appears in a peer-reviewed article in a well-regarded journal.  If time permits, we may discuss what should be done when one discovers an error like this (and compare with what I actually did).  

Document Actions