J. Roger Hindley, Homepage

E-address: hindley[at]waitrose.com

Field of Interest

Mathematical logic; particularly lambda-calculus, combinatory logic and type-theories, with a current bias towards historical aspects.
      Lambda-calculus and combinatory logic are formal systems, to some extent rivals, used in the construction and study of programming languages which are higher-order (i.e. in which programs may change other programs). These two systems were invented in the 1920s by mathematicians for use in higher-order logic, and came to be applied in programming theory from the 1970s onward, when that theory expanded to cover higher-order computations.
      In a type-theory, types are labels which may be attached to certain programs to show what other programs they can change. A type-system is a particular set of rules for attaching types; the rules themselves are usually reasonably simple, but such questions as what programs are typable, what set of types a program may receive, and whether a typable computation can continue for ever, are not always easy to answer and have occupied the efforts of many researchers.

Files for Downloading

These files for downloading are PDF files, and require Adobe Acrobat or Acrobat Reader. They are available for personal use, not for re-distribution or for commerce or financial profit. Their copyright belongs to their authors.

For book "Basic Simple Type Theory" (published by Cambridge University Press, 1997 and 2008):
  • Errata-list (produced by the author; last updated 20 December 2012).

  • For book "Lambda-calculus and Combinators, an Introduction" (co-author J. P. Seldin, published by Cambridge University Press, 2008):
  • Errata-list (produced by the authors; last updated 7 April 2017).
  • Supplement "Goedel's Consistency-proof for Arithmetic" (a revised version of Chapter 18 in the 1986 edition, which was omitted from the present edition due to lack of space.)

  • For article "Lambda-calculus and Combinators in the 20th Century" (co-author F. Cardone; in "Handbook of the History of Logic", "Volume 5: Logic from Russell to Church", pp. 723--817; edited by D. M. Gabbay and J. Woods, published by Elsevier (North-Holland), Amsterdam, 2009):
  • Errata-list (produced by the authors; last updated 30 January 2010);
  • Contents page (produced by the authors);
  • Preprint version of article (date 2006; from Swansea University Mathematics Research Report No. MRRS-05-06 "History of Lambda-calculus and Combinatory Logic"; differs from published article in very few places).

  • Ph.D. thesis: "The Church-Rosser Property and a Result in Combinatory Logic", University of Newcastle upon Tyne, 1964. (8.5 MB file) (this copy is provided by courtesy of Pierre Lescanne's website of historical sources at the E.N.S., Lyon, France, and omits a now-redundant chapter, Ch.6).

    Note: "Lambda-Calculus Conferences in the 1970s" plus Swansea 1979 conference group photo and its key to names.

    Note: "The Root-2 proof as an example of non-constructivity".




    Basic Simple Type Theory; Cambridge University Press, 1997, 2008. MathSciNet MR1466699. An Errata-list is available; see Files for Downloading above.

    (Co-author J. P. Seldin) Lambda-calculus and Combinators, an Introduction; Cambridge University Press, 2008. (Earlier edition was 1986 with title Introduction to Combinators and Lambda-calculus.) An Errata-list is available, also a supplementary chapter on Goedel's consistency-proof for arithmetic; see Files for Downloading above.

    (Co-authors B. Lercher, J. P. Seldin) Introduction to Combinatory Logic; Cambridge University Press, 1972, No.7 in series "London Mathematical Society Lecture Notes". ( MathSciNet MR0335242.)

    (Co-authors H. B. Curry, J. P. Seldin) Combinatory Logic, Volume 2; North-Holland Co., Amsterdam, 1972, No.65 in series "Studies in Logic".

    (Edited; co-editor J. P. Seldin) To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism Academic Press, London and New York, 1980. ( MathSciNet MR0592792.)

    (Edited; co-editor P. de Groote) Typed Lambda Calculi and Applications, Proceedings of the Third International Conference TLCA '97, Nancy, France; Springer-Verlag, Berlin and Heidelberg, 1997. No.1210 in series "Lecture Notes in Computer Science".


    (Co-author Mariangiola Dezani-Ciancaglini) Lambda Calculus. In Wiley Encyclopedia of Computer Science and Engineering, Volume 3, pp. 1701--1708, edited by Benjamin Wah; published by Wiley, 2008.

    Curry's last problem: imitating lambda-beta-reduction in combinatory logic, Proc. 32nd MLG Meeting, Shizuoka, Japan, November 26--28, 1998, pp. 20--22. PDF of preprint.

    M. H. Newman's typability algorithm for lambda-calculus, Journal of Logic and Computation 18(2) (April 2008), 229--238. PDF of preprint.

    (Co-author F. Cardone) Lambda-calculus and combinators in the 20th century. In Handbook of the History of Logic, Volume 5: Logic from Russell to Church, edited by D. M. Gabbay and J. Woods, published by Elsevier (North-Holland Co.), Amsterdam, 2009, pp. 723--817. PDFs of preprint and Errata list: see Files for Downloading above.

    (Co-author N. Çağman) Combinatory Weak Reduction in Lambda Calculus, Theoretical Computer Science 198 (1998), 239--247. ( MathSciNet MR1616965.) PDF available here.

    (Co-author M. W. Bunder) Two beta-equal lambda-I-terms with no types in common, Theoretical Computer Science 155 (1996), 265--266. ( MathSciNet MR1379073.) PDF available here.

    (Co-authors P. Trigg, M. W. Bunder) Combinatory abstraction using B, B' and friends, Theoretical Computer Science 135 (1994), 405--422. ( MathSciNet MR1311210.) PDF available here.

    BCK and BCI logics, condensed detachment and the 2-property, Notre Dame Journal of Formal Logic 34 (1993), 231--250. ( MathSciNet MR1231287.) PDF available here.

    Types with intersection: an introduction, Formal Aspects of Computing 4 (1992), 470--486. PDF: see SpringerLink.

    (Co-author Mariangiola Dezani-Ciancaglini) Intersection types for combinatory logic, Theoretical Computer Science 100 (1992), 303--324. ( MathSciNet MR1173628.) PDF: see Science Direct.

    (Co-author D. Meredith) Principal type-schemes and condensed detachment, Journal of Symbolic Logic 55 (1990), 90--105. ( MathSciNet MR1043546.) PDF: here, or see Project Euclid.

    (Co-authors M. W. Bunder, J. P. Seldin) On adding (ξ) to weak equality in combinatory logic, Journal of Symbolic Logic 54 (1989), 590--607. ( MathSciNet MR0997891.) PDF: see Project Euclid.

    BCK-combinators and linear λ-terms have types, Theoretical Computer Science 64 (1989), 97--105. ( MathSciNet MR0993977.) PDF: see Science Direct.

    Combinators and lambda-calculus, a short outline. In Combinators and Functional Programming Languages, edited by G. Cousineau, P.-L. Curien and B. Robinet, no.242 in series "Lecture Notes in Computer Science", Springer-Verlag, Berlin, 1985. Pp. 104--122. PDF here.

    Coppo-Dezani types do not correspond to propositional logic, Theoretical Computer Science 28 (1984), 235--236. PDF: see Science Direct.

    Curry's type-rules are complete with respect to the F-semantics too, Theoretical Computer Science 22 (1983), 127--133. PDF: see Science Direct.

    The completeness theorem for typing lambda terms, Theoretical Computer Science 22 (1983), 1--17. ( MathSciNet MR0693047.) PDF: see Science Direct.

    The simple semantics for Coppo-Dezani-Sallé types. In International Symposium on Programming, 5th Colloquium, Proceedings 1982, edited by M. Dezani and U. Montanari, no.137 in series "Lecture Notes in Computer Science", Springer-Verlag, Berlin, 1982. Pp. 212--226. ( MathSciNet MR0807180.) PDF: see SpringerLink.

    (Co-author G. Longo) Lambda-calculus models and extensionality, Zeitschrift fur Mathematische Logik 26 (1980), 289--310. ( MathSciNet MR0582407.) PDF: see Wiley Online Library.

    The discrimination theorem holds for combinatory weak reduction, Theoretical Computer Science 8 (1979), 393--394. PDF: see Science Direct.

    Standard and normal reductions, Transactions of the American Mathematical Society 241 (1978), 253--271. ( MathSciNet MR0492300.) PDF: see Jstor.

    Reductions of residuals are finite, Transactions of the American Mathematical Society 240 (1978), 345--361. ( MathSciNet MR0489603.) PDF: see Jstor.

    The equivalence of complete reductions, Transactions of the American Mathematical Society 229 (1977), 227--248. ( MathSciNet MR0444445.) PDF: see Jstor.

    (Co-author G. Mitschke) Some remarks about the connections between combinatory logic and axiomatic recursion theory, Archiv fur Mathematische Logik 18 (1977), 99--103. ( MathSciNet MR0469717.) PDF: see SpringerLink.

    Combinatory reductions and lambda reductions compared, Zeitschrift fur Mathematische Logik 23 (1977), 169--180. ( MathSciNet MR0485229.) PDF available here.

    An abstract Church-Rosser theorem, II: applications, Journal of Symbolic Logic 39 (1974), 1--21. ( MathSciNet MR0347558.) PDF: see Project Euclid.

    (Co-author B. Lercher) A short proof of Curry's normal form theorem, Proceedings of the American Mathematical Society 24 (1970), 808--810. ( MathSciNet MR0255405.) PDF: see Jstor.

    The principal type-scheme of an object in combinatory logic, Transactions of the American Mathematical Society 146 (1969), 29--60. ( MathSciNet MR0253905.) PDF: here, or Jstor.

    An abstract form of the Church-Rosser theorem, I, Journal of Symbolic Logic 34 (1969), 545--560. ( MathSciNet MR0302434.) PDF: see Project Euclid.

    Axioms for strong reduction in combinatory logic, Journal of Symbolic Logic 32 (1967), 224--236. ( MathSciNet MR0214470.) PDF: see Project Euclid.