Sciweavers

Share
TPHOL
2008
IEEE

Certifying a Termination Criterion Based on Graphs, without Graphs

8 years 8 months ago
Certifying a Termination Criterion Based on Graphs, without Graphs
Although graphs are very common in computer science, they are still very difficult to handle for proof assistants as proving properties of graphs may require heavy computations. This is a problem when it comes to issues such as the certification of a proof of well-foundedness, since premises of generic theorems involving graph properties may be at least as difficult to prove as their conclusion. We define a framework and propose an original approach based on both shallow and deep embeddings for the mechanical certification of these kinds of proofs without the help of any graph library. This framework actually avoids concrete models of graphs and handles those implicitly. We illustrate this approach on a powerful refinement of the dependency pairs approach for proving termination. This refinement makes heavy use of graph analysis and our technique is powerful enough to deal efficiently –and with full automation– with graphs containing thousands of arcs, as they may occur in ...
Pierre Courtieu, Julien Forest, Xavier Urbain
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Pierre Courtieu, Julien Forest, Xavier Urbain
Comments (0)
books