J. Roger Hindley, 2nd Homepage

Supplement to main homepage, which is on the Swansea University website at this address.

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 12 July 2011).
  • 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 a few passages).

    • Ph.D. thesis: available on Pierre Lescanne's website of historical sources at the E.N.S., Lyon, France.
    (Title: "The Church-Rosser Property and a Result in Combinatory Logic", Mathematics Department, University of Newcastle upon Tyne, England, 1964. Chapter 6 (now redundant) is omitted from this copy.)

    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".

    ___

    Publications

    (Most of the following are also listed on main homepage.)

    Books:

    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".

    Papers:

    (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: 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: see Wiley Online Library. .

    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: see 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.