12
$\begingroup$

I have some background in set theory and automata and I am looking for a good place to start with lambda calculus.

$\endgroup$
1
  • $\begingroup$ I suspect it'd help to distinguish typed and untyped lambda calculus, since they're quite different subjects. $\endgroup$ Commented Mar 30, 2015 at 0:52

7 Answers 7

7
$\begingroup$

There is, of course, the very famous book by Barendregt,

  • The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Revised Edition, North-Holland, 1985. (link to vendor)

which doesn't require much background except for the usual mathematical maturity. This is mostly about the untyped lambda calculus. He also has some introductory notes here.

$\endgroup$
3
  • $\begingroup$ Link to the notes is broken - would it be possible to update it. $\endgroup$
    – user85079
    Commented Jan 9, 2016 at 14:54
  • $\begingroup$ @Mika'il The link to the notes works absolutely fine for me. $\endgroup$ Commented Jan 9, 2016 at 15:44
  • $\begingroup$ The link to book now returns 404 not found. $\endgroup$
    – wlnirvana
    Commented Mar 16, 2017 at 2:49
4
$\begingroup$

An introductory book that seems very nice to me is Lambda-Calculus and Combinators. An introduction by J. Roger Hindley and Jonathan P. Seldin.

$\endgroup$
1
  • $\begingroup$ Plus it has exercises and some of them have solutions. $\endgroup$ Commented Aug 14, 2013 at 8:41
4
$\begingroup$

The best books that I've found are:

  • Very basic: Hankin, An introduction to the lambda calculus for computer scientists.
  • Advanced: Sorensen and Urzyczyn, Lectures on the Curry-Howard isomorphism.
  • Advanced: Hindley, Basic simple type theory.
  • The Bible: Barendregt, The lambda calculus: its syntax and semantics.
$\endgroup$
4
$\begingroup$

Another excellent book is "Lambda-calculus, types and models" Ellis Horwood (1993) by Jean-Louis Krivine http://www.pps.jussieu.fr/~krivine/articles/Lambda.pdf

$\endgroup$
1
2
$\begingroup$

I really enjoy Types and Programming Languages by Benjamin C. Pierce. We used this for a course on the lambda calculus, and I felt this was a great way for a mathematician to learn the subject

$\endgroup$
1
$\begingroup$

Stoy's book:

Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977

Is a classic, and highly recommended.

$\endgroup$
1
$\begingroup$

Proof and Types is a good place to learn about the Curry-Howard isomorphism.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .