[Club2] Fr. 8.8., 10h30 im Turing (MI 00.09.055)

[Alexander Krauss]

Liebe Leute,

Nächsten Freitag (8.8.) um 10h30 trage ich im Turing vor. Danach kommt 
vermutlich noch Sascha dran, es gibt also wieder eine Doppel-Session.



                             Alex Krauss:

                      Shallow Dependency Pairs

            (Probevortrag TPHOLs 08, "Emerging Trends")

We show how the dependency pair approach, commonly used to modularize
termination proofs of rewrite systems, can be adapted to establish
termination of recursive functions in a system like Isabelle/HOL or
Coq. It turns out that all that is required are two simple lemmas
about wellfoundedness.