26
$\begingroup$

There are many classic textbooks in set and category theory (as possible foundations of mathematics), among many others Jech's, Kunen's, and Awodey's.

Are there comparable classic textbooks in type theory, introducing and motivating their matter in a generally agreed upon manner from the ground up and covering the whole field, essentially?

If not so: why?

  • 0
    Girard's _Proofs and Types_ is quite well-regarded, I think. But one needs some background in ordinary first-order logic to understand it.2012-02-25
  • 0
    Why would you insist on [set-theory] here?2012-02-25
  • 0
    @Asaf: Because I know set theory as one way of foundation and do believe type theory to be an alternative way of foundation. The one road is clear to me (by lots of agreed upon material), the other one not so clear.2012-02-25
  • 0
    @Zhen Lin: There is lot of set theoretic material to be understood without a lot of background. Why is such material so hard to find in type theory? (No agreed upon ontology, no agreed upon terminology, no agreed upon symbology, ...?)2012-02-25
  • 0
    @Zhen Lin: In any case, thanks a lot for the reminder. I do have Girard's book on my computer and I will definitely give it a (re)read.2012-02-25
  • 0
    But @Hans, this question is *nothing* about set theory. It is about *type theory*. The only connection to set theory is that it can be used as a foundation of mathematics. By that logic, add [category-theory] and so on.2012-02-25
  • 0
    I could and I should do so. Because set theory, type theory and category theory are so deeply intermingled (see http://www.andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf). The question remains: where are the classic textbooks in type theory (compared to those in set and category theory)?2012-02-25
  • 1
    A very clear exposition on basic level with connections to programming languages is Pierce's _Types and Programming Languages_; there is also a sequel _Advanced Topics in Types and Programming Languages_.2012-02-25

2 Answers 2