Reducibility of Types in Typed Lambda Calculus: Comment on a Paper by Richard Statman - Wil Dekkers (Inf. Comput., 1988)

Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus. - Henk Barendregt; Martin W. Bunder; Wil Dekkers (J. Symb. Log., 1993)

Inhabitation of Types in the Simply Typed Lambda Calculus - Wil Dekkers (Inf. Comput., 1995)

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus. - Wil Dekkers; Martin W. Bunder; Henk Barendregt (Arch. Math. Log., 1998)

Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic into Illative Combinatory Logic. - Wil Dekkers; Martin W. Bunder; Henk Barendregt (J. Symb. Log., 1998)

Pure Type Systems with More Liberal Rules. - Martin W. Bunder; Wil Dekkers (J. Symb. Log., 2001)

Are there Hilbert-style Pure Type Systems? - Martin W. Bunder; Wil Dekkers (Log. Methods Comput. Sci., 2008)

Weak mu-equality is decidable - Wil Dekkers (CoRR, 2011)

Lambda Calculus with Types. - Hendrik Pieter Barendregt; Wil Dekkers; Richard Statman (Cambridge University Press, 2013)

Automata Theoretic Account of Proof Search. - Aleksy Schubert; Wil Dekkers; Hendrik Pieter Barendregt (CSL, 2015)