4
$\begingroup$

Can someone recommend me a book for self study which will cover topics of logic, lambda calculus and type theory. I know about "Computability and Logic" written by Bolos but it describe recursive function as a model of computation and does no cove type theory.

If there is no singe book I would like to read some book which would build a bridge between those topics.

$\endgroup$
  • $\begingroup$ Did you take a look at this question? It seems that many references there could help you further. Perhaps it can even be considered a duplicate? $\endgroup$ – Lord_Farin May 27 '13 at 13:57
  • 1
    $\begingroup$ I loved "Lectures on the Curry-Howard Isomorphism" by Sørensen and Urzyczyn, but it's possible that it will assume too much of the lambda-calculus background. You might try it and see. $\endgroup$ – MJD May 27 '13 at 14:58
  • $\begingroup$ @Lord_Farin question you pointed is specifically about lambda calculus and I am asking about connection between logic and computability (lambda calculus). $\endgroup$ – Trismegistos May 28 '13 at 7:02
2
$\begingroup$

I found some good book on those topics. This book has exercises with solution so it is perfect for self studying. The book is "Lambda-Calculus and Combinators an Introduction" by J. Roger Hindley, Jonathan P. Seldin. Link for more info http://www.cambridge.org/us/knowledge/isbn/item1175709/?site_locale=en_US

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

I found this a valuable and concise introduction:

The Seven Virtues of Simple Type Theory by William M. Farmer.

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

Being a programmer the one I am recommending is more of a programming book but does cover lambda calculus and type theory. Types and Programming Languages by Benjamin C. Pierce. I am not sure what you mean by logic in this question so I am not saying the book covers logic, but am pretty sure it will cover what you need.

For the list of lambda type systems covered see: λ-Calculus extensions: meaning of extension symbols

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ I have read some parts of "Types and Programming Languages" by Benjamin C. Pierce. It explained more practical aspects (if you can say so about lambda-calculus) of lambda-calculus and I have to admin it was quite good. $\endgroup$ – Trismegistos Mar 20 '14 at 15:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.