Recomendation for CS type theory book

Stream: new members

[Miguel Negrão]

Hi all,

Which book on type theory would you recommend from a CS perpective which covers the basics, and things such as simply typed lambda calculus, system F, intuitionistic type theory, calculus of constructions ?

Would you recommend Robert Harper's Practical Foundations for Programming Languages ?

Thanks

[Bulhwi Cha]

Below are the paper and the books I want to read in the future:

• The Seven Virtues of Simple Type Theory
• Introduction to Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

[Miguel Negrão]

Thanks !

[Miguel Negrão]

"The Seven Virtues of Simple Type Theory" seems like a short introduction, might be a good place to start.

[Logan Murphy]

This doesn't cover everything you mentioned, but for an introductory type theory book I would also mention Type Theory & Functional Programming by Simon Thompson.

[Jonathan Whitehead]

I'm quite new here but I read the HoTT book from time to time. As I get better and better, the book gets better and better but it was inaccessible to me for a long time. I have another book that was a bit easier but quite laborious to read. It's called

Type Theory and Formal Proof An Introduction by Nederpelt and Geuvers

It covers the topics you mentioned and was one of the first books I could actually read. I didn't see a free version and it's quite expensive.

[Miguel Negrão]

@Jonathan Whitehead Thanks ! I will have a look at "Type Theory and Formal Proof An Introduction".