Termination Analysis of the Untyped lamba-Calculus. - Neil D. Jones; Nina Bohr (RTA, 2004)

Relational Reasoning for Recursive Types and References. - Nina Bohr; Lars Birkedal (APLAS, 2006)

Call-by-Value Termination in the Untyped lambda-Calculus. - Neil D. Jones; Nina Bohr (Log. Methods Comput. Sci., 2008)