Big trees in a lambda - calculus with lambda - expressions as types. - Roel C. de Vrijer (Lambda-Calculus and Computer Science Theory, 1975)

A Direct Proof of the Finite Developments Theorem. - Roel C. de Vrijer (J. Symb. Log., 1985)

Extending the Lambda Calculus with Surjective Pairing is Conservative - Roel C. de Vrijer (LICS, 1989)

Unique Normal Forms for Lambda Calculus with Surjective Pairing - Jan Willem Klop; Roel C. de Vrijer (Inf. Comput., 1989)

Extended Term Rewriting Systems. - Jan Willem Klop; Roel C. de Vrijer (CTRS, 1990)

Modularity of Confluence: A Simplified Proof. - Jan Willem Klop; Aart Middeldorp; Yoshihito Toyama; Roel C. de Vrijer (Inf. Process. Lett., 1994)

Completing Partial Combinatory Algebras With Unique Head-Normal Forms. - Inge Bethke; Jan Willem Klop; Roel C. de Vrijer (LICS, 1996)

Extending partial combinatory algebras. - Inge Bethke; Jan Willem Klop; Roel C. de Vrijer (Math. Struct. Comput. Sci., 1999)

Descendants and Origins in Term Rewriting. - Inge Bethke; Jan Willem Klop; Roel C. de Vrijer (Inf. Comput., 2000)

A geometric proof of confluence by decreasing diagrams. - Jan Willem Klop; Vincent van Oostrom; Roel C. de Vrijer (J. Log. Comput., 2000)

A Calculus of Lambda Calculus Contexts. - Mirna Bognar; Roel C. de Vrijer (J. Autom. Reason., 2001)

Four equivalent equivalences of reductions. - Vincent van Oostrom; Roel C. de Vrijer (WRS, 2002)

Infinitary Normalization. - Jan Willem Klop; Roel C. de Vrijer (We Will Show Them! (2), 2005)

Iterative Lexicographic Path Orders. - Jan Willem Klop; Vincent van Oostrom; Roel C. de Vrijer (Essays Dedicated to Joseph A. Goguen, 2006)

Reduction Under Substitution. - Jörg Endrullis; Roel C. de Vrijer (RTA, 2008)

Proving Infinitary Normalization. - Jörg Endrullis; Clemens Grabmayer; Dimitri Hendriks; Jan Willem Klop; Roel C. de Vrijer (TYPES, 2008)

Lambda calculus with patterns. - Jan Willem Klop; Vincent van Oostrom; Roel C. de Vrijer (Theor. Comput. Sci., 2008)

Local Termination. - Jörg Endrullis; Roel C. de Vrijer; Johannes Waldmann (RTA, 2009)

Local Termination: theory and practice - Jörg Endrullis; Roel C. de Vrijer; Johannes Waldmann (Log. Methods Comput. Sci., 2010)