In this talk, I will discuss tuple interpretation based technique to capture the BFF, which is a class of second order functionals that can be computed by Oracle Turing Machines in Polynomial time. This class of functionals is conjectured to be the natural higher-order counterpart to the poly time computable functions in the first-order setting. We provide sufficient conditions so that if a higher-order rewriting system that computes a type-2 functional over N and such that it admits a polynomially bounded tuple interpretation, then such functional lies in the BFF class.

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabilistic setting in order to prove almost-sure innermost termination of probabilistic TRSs. To evaluate its power, we implemented the new framework in our tool AProVE.

Morphic sequences form a natural class of infinite sequences, extending the well-studied class of automatic sequences. Where automatic sequences are known to have several equivalent characterizations and the class of automatic sequences is known to have several closure properties, for the class of morphic sequences only similar closure properties were known. In this talk we give a number of equivalent characterizations of morphic sequences. In particular, we extend the automaton-based definition of automatic sequences to a generalization exactly covering the morphic sequences, we give a characterization of morphic sequences by finiteness of a particular class of subsequences, we relate morphic sequences to rationality of infinite terms and we describe them by infinitary rewriting. Morphic sequences are of special interest as they give rise to exciting turtle visualization, of which we give several examples. This is also the main topic of the book as it appeared recently in Dutch, and is expected to appear in English soon.