[PRL] POPL Trip Report

[Mitchell Wand]

What I had in mind was that they were annotating arcs of the control-flow
graph with notations about size transition, whereas you guys were annotating
them with formulas, so you could eliminate arcs that whose formulae were
unsatisfiable.  But I'll talk to Aaron about this when I see him later this
week.

--Mitch

On Jan 10, 2008 2:58 PM, Matt Might <matt at might.net> wrote:

> 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
>
>
-------------- next part --------------
HTML attachment scrubbed and removed