FLoC
MEETINGS
PROGRAM
FACILITIES
SEATTLE
ORGANIZATION
MISCELLANEOUS
OUTOFDATE

WST on Tuesday, August 15th
09:00‑10:00 
Byron Cook
(Microsoft Research Cambridge)
Program termination analyses for free! [ppt]
I will describe an easytofollow recipe for the construction of
automatic program termination analyses. The recipe's primary ingredient
is an abstractinterpretationbased program analysis for invariance
properties  any one will do. If we change the underlying program
analysis, we get a different program termination analysis.

10:30‑11:00 
Peter SchneiderKamp
(RWTH Aachen)
Juergen Giesl
(RWTH Aachen)
Alexander Serebrenik
(TU Eindhoven)
Rene Thiemann
(RWTH Aachen)
Termination Analysis for Logic Programs by Term Rewriting Revisited
There are two kinds of approaches for termination analysis of logic programs:
"transformational" and "direct" ones. Direct approaches prove termination
directly on the basis of the logic program. Transformational approaches
transform a logic program into a term rewrite system (TRS) and then analyze
termination of the resulting TRS instead. Thus, transformational approaches
make all methods previously developed for TRSs available for logic programs as
well. However, the applicability of most existing transformations is quite
restricted, as they can only be used for certain subclasses of logic programs.
(Most of them are restricted to wellmoded programs.)
In this paper we improve these transformations such that they become applicable
for any definite logic program. Moreover, we show that our transformation
results in TRSs which are indeed suitable for automated termination analysis.
In contrast to most other methods for termination of logic programs, our
technique is also sound for logic programming without occur check, which is
typically used in practice. We implemented our approach in the termination
prover AProVE and successfully evaluated it on a large collection of examples.

11:00‑11:30 
Manh Thang Nguyen (DTAI group, Department of Computer Science, K.U.Leuven, Belgium.)
Maurice Bruynooghe (DTAI group, Department of Computer Science, K.U.Leuven, Belgium)
Danny De Schreye (DTAI group, Department of Computer Science, K.U.Leuven, Belgium)
Michael Leuschel
(HeinrichHeineUniversität Düsseldorf)
Program Specialisation as a Preprocessing Step for Termination Analysis
Analysing the structure of logic programs may provide useful information for termination analysis in Logic Programming (LP).
In this paper, we present a simple transformation technique for termination analysis in LP based on the structural information of the program. We report on an extensive experiment which shows that this technique can significantly improve the precision of termination analysis and can be applied as a preprocessing step in any LP termination analyser.

11:30‑12:00 
Naoki Nishida
(Nagoya University)
Koichi Miura (Nagoya University)
Dependency Graph Method for Proving Termination of Narrowing
Term rewriting systems with extra variables are useful to represent
operators for inverse computation. Their ground rewrite sequences can be
simulated by narrowing sequences starting from the same initial
terms. In this paper we refine the dependency pair method for proving
termination of narrowing, and extend the dependency graph method for
proving termination of rewriting to a method for narrowing.

12:00‑12:30 
Yi Wang (Nagoya University)
Masahiko Sakai
(Graduate School of Infomation Science, Nagoya University)
On Nonlooping Term Rewriting
Proving nontermination is important for instance if one wants to decide termination for a given class of TRSs. Although the usual method is to find looping reduction sequences, there are nonlooping infinite reduction sequences. We find some new interesting nonlooping examples and propose new definitions to classify them. We also show the undecidability of existence of nonlooping sequence.

14:00‑14:30 
Frederic Blanqui
(INRIA)
Higherorder dependency pairs
Art and Giels proved that the termination of a firstorder rewrite
system can be reduced to the study of its ``dependency pairs''. We
extend these results to rewrite systems on simply typed
lambdaterms by using Tait's computability technique.

14:30‑15:00 
Wojciech Moczydlowski
(Cornell University)
Normalization of intuitionistic set theories
IZF is a wellinvestigated impredicative constructive counterpart of ZermeloFraenkel set theory. We define weaklynormalizing lambda calculus $\lambda Z$ corresponding to proofs in an intensional version of IZF with Replacement according to the CurryHoward isomorphism principle. By adapting a counterexample invented by M. Crabbe, we show that $\lambda Z$ does not strongly normalize. Moreover, we prove that the calculus corresponding to a nonwellfounded IZF does not even weakly normalize. Thus $\lambda Z$ and IZF are positioned on the fine line between weak, strong and lack of normalization.

16:00‑16:30 
Joerg Endrullis
(Vrije Universiteit Amsterdam)
Dieter Hofbauer
(Univ. Kassel)
Johannes Waldmann
(HTWK Leipzig, FB IMN)
Decomposing Terminating Rewrite Relations
We decompose an arbitrary rewrite relation
into the product of a contextfree system
and an inverse contextfree system with empty righthand sides.
By requiring both of these relations to be terminating,
we lose computational completeness
and arrive at the class of deleting rewriting systems.
Our new treatment allows to efficiently
construct the rewrite closure of a regular language
with respect to deleting or matchbounded rewriting.
Previous implementations of this method
either used a complete but inefficient
decomposition algorithm
leading to impracticable resource consumption,
or incomplete approximation algorithms.
Our new algorithm is both efficient and exact,
thereby improving the power of automated termination provers
that use the method of matchbounds.

16:30‑17:00 
Hans Zantema
(Technische Universiteit Eindhoven)
Termination of Extended String Rewriting
We extend string rewriting in such a way that in the rules also
variables may occur that may be replaced by arbitrary strings. This is a
natural format occurring in text editing and pattern matching.
We investigate termination behaviour of these extended string rewriting
systems.


