Axioms for Strong Reduction in Combinatory Logic. - J. Roger Hindley (J. Symb. Log., 1967)

An Abstract Form of the Church-Rosser Theorem. I. - J. Roger Hindley (J. Symb. Log., 1969)

Introduction to combinatory logic. - J. Roger Hindley; Rasmus Lerdorf; Jonathan P. Seldin (Cambridge University Press, 1972)

An Abstract Church-Rosser Theorem. II: Applications. - J. Roger Hindley (J. Symb. Log., 1974)

Combinatory Reductions and Lambda Reductions Compared. - J. Roger Hindley (Math. Log. Q., 1977)

The Discrimination Theorem Holds for Combinatory Weak Reduction. - J. Roger Hindley (Theor. Comput. Sci., 1979)

The simple semantics for Coppe-Dezani-Sallé types. - J. Roger Hindley (Symposium on Programming, 1982)

The Completeness Theorem for Typing lambda-Terms. - J. Roger Hindley (Theor. Comput. Sci., 1983)

Curry's Type-Rules are Complete with Respect to the F-Semantics too. - J. Roger Hindley (Theor. Comput. Sci., 1983)

Coppo-Dezani Types do not Correspond to Propositional Logic. - J. Roger Hindley (Theor. Comput. Sci., 1984)

Combinators and Lambda-Calculus. - J. Roger Hindley (Combinators and Functional Programming Languages, 1985)

Introduction to Combinators and Lambda-Calculus. - J. Roger Hindley; Jonathan P. Seldin (Cambridge University Press, 1986)

On Adding (xi) to Weak Equality in Combinatory Logic. - Martin W. Bunder; J. Roger Hindley; Jonathan P. Seldin (J. Symb. Log., 1989)

BCK-Combinators and Linear lambda-Terms have Types. - J. Roger Hindley (Theor. Comput. Sci., 1989)

Principal Type-Schemes and Condensed Detachment. - J. Roger Hindley; David Meredith 002 (J. Symb. Log., 1990)

Types with Intersection: An Introduction. - J. Roger Hindley (Formal Aspects Comput., 1992)

Intersection Types for Combinatory Logic. - Mariangiola Dezani-Ciancaglini; J. Roger Hindley (Theor. Comput. Sci., 1992)

BCK and BCI Logics, Condensed Detachment and the 2-Property. - J. Roger Hindley (Notre Dame J. Formal Log., 1993)

Combinatory Abstraction Bsing B, B' and Friends. - P. Trigg; J. Roger Hindley; Martin W. Bunder (Theor. Comput. Sci., 1994)

Two beta-Equal lambda-I-Terms with no Types in Common. - Martin W. Bunder; J. Roger Hindley (Theor. Comput. Sci., 1996)

Combinatory Weak Reduction in Lambda Calculus. - Naim Çagman; J. Roger Hindley (Theor. Comput. Sci., 1998)

M. H. Newman's Typability Algorithm for Lambda-calculus. - J. Roger Hindley (J. Log. Comput., 2008)

Lambda-Calculus. - Mariangiola Dezani-Ciancaglini; J. Roger Hindley (Wiley Encyclopedia of Computer Science and Engineering, 2008)

Lambda-Calculus and Combinators in the 20th Century. - Felice Cardone; J. Roger Hindley (Logic from Russell to Church, 2009)