Towards Correctness of Program Transformations Through Unification and Critical Pair Computation - Conrad Rau; Manfred Schmidt-Schauß (UNIF, 2010)

A Unification Algorithm to Compute Overlaps in a Call-by-Need Lambda-Calculus with Variable-Binding Chains. - Conrad Rau; Manfred Schmidt-Schauß (UNIF, 2011)

Correctness of Program Transformations as a Termination Problem. - Conrad Rau; David Sabel; Manfred Schmidt-Schauß (IJCAR, 2012)

Algorithms for Extended Alpha-Equivalence and Complexity. - Manfred Schmidt-Schauß; Conrad Rau; David Sabel (RTA, 2013)