[PRL] POPL Trip Report

[Matt Might]

On Jan 10, 2008 10:48 AM,  <turon at ccs.neu.edu> wrote:
>
>
> > ================================================================
> >
> > 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.

I've spoken to Neil and Damien Sereni about their work on termination
and how it relates to stuff I do.  They seem more interested in the
precision-enhancing effects of abstract garbage collection from
Gamma-CFA than in the propositional aspects of LFA.

Damien told me that the power of their termination analysis is a
function of the precision of their control-flow analysis.

-Matt