[PRL] POPL Trip Report

[turon at ccs.neu.edu]

> ================================================================ 
> 
> Lunch: Spoke to Neil Jones. He's retired now, but is finishing off 
> a journal paper on termination analysis for untyped LC. He uses CFA 
> to make a control-flow graph, and then counts changes in the size of 
> the environment along each edge. The moral is that if every cycle in 
> the control-flow graph is net decreasing, your term terminates. 
> 
> This appears to be enough to prove termination for lots of interesting 
> terms, including factorial (written with Y!), Ackermann's function, 
> etc., even using Churh numerals. 
> 
> This sounds a lot like Matt Might's Logic-Flow Analysis. Aaron, can 
> you say offhand how close this might be to what you did for Pete? 
> 
> I invited him to stop by the next time he's in the US, so he could 
> talk to Olin, Harry, et al. 
> 
> ================================================================ 

In the formalization of this work that I'm familiar with, there is no use of (or need for) a theorem prover.  So I'm not sure about the connection to Logic-Flow Analysis.

The basic approach is to instrument a standard 0CFA analysis with some additional data-flow information, in particular tracking the flow of data into and out of environments.  This flow information, together with an appropriate notion of a call-graph, is sufficient to do termination analysis.

As far as the relation to my work last semester: in fact, I used this framework as a starting point for my analysis.  However, I add an additional layer, modeled after Manolios and Vroon's Calling Context Graphs, which uses a theorem prover to strengthen the analysis.