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

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.