30
$\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?

$\endgroup$
8
  • $\begingroup$ Girard's Proofs and Types is quite well-regarded, I think. But one needs some background in ordinary first-order logic to understand it. $\endgroup$
    – Zhen Lin
    Feb 25, 2012 at 0:24
  • $\begingroup$ Why would you insist on [set-theory] here? $\endgroup$
    – Asaf Karagila ♦
    Feb 25, 2012 at 0:26
  • $\begingroup$ @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. $\endgroup$
    – Hans-Peter Stricker
    Feb 25, 2012 at 0:30
  • $\begingroup$ @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, ...?) $\endgroup$
    – Hans-Peter Stricker
    Feb 25, 2012 at 0:33
  • 1
    $\begingroup$ 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. $\endgroup$
    – sdcvvc
    Feb 25, 2012 at 2:17

2 Answers 2

Reset to default
25
$\begingroup$

Although not as comprehensive a textbook as, say, Jech's classic book on set theory, Jean-Yves Girard's Proofs and Types is an excellent starting point for reading about type theory. It's freely available from translator Paul Taylor's website as a PDF. Girard does assume some knowledge of the lambda calculus; if you need to learn this too, I recommend Hindley and Seldin's Lambda-Calculus and Combinators: An Introduction.

As others have mentioned, Martin-Löf's Intuitionistic Type Theory would then be a good next step.

A different approach would be to read Benjamin Pierce's wonderful textbook, Types and Programming Languages. This is oriented towards the practical aspects of understanding types in the context of writing programming languages, rather than purely its mathematical characteristics or foundational promise, but nonetheless it's a very clear and well-written book, with numerous exercises.

The bibliography provided by the Stanford Encyclopedia of Philosophy entry on type theory is quite extensive, and might provide alternative avenues for your research.

$\endgroup$
0
8
$\begingroup$

There are two main settings in which I see type theory as a foundational system.

The first is intuitionistic type theory, particularly the system developed by Martin-Löf. The book Intuitionistic Type Theory (1980) seems to be floating around the internet.

The other setting is second-order (and higher-order) arithmetic. Two main books on this are Foundations without foundationalism by Stewart Shapiro (1991) and Subsystems of second order arithmetic by Stephen Simpson (1999). A decent amount of constructive mathematics, for example the material in Constructive Analysis by Bishop and Bridges (1985), can also be formalized directly in constructive higher-order arithmetic, however the taste of many constructivists is to avoid doing this.

$\endgroup$
3
  • $\begingroup$ +1 Nice! (1) What is " a foundational system"? Is it a special kind of formal system? (2) What are relations and differences between set theory, logic, type theory and lambda calculus? I have never been able to understand their purposes even after reading Wiki. (3) Wiki says type theory serves as an alternative to Naive set theory. So I wonder if type theory is a kind of axiom set theory, just like ZFC is a kind of axiom set theory? $\endgroup$
    – Tim
    Feb 25, 2012 at 13:31
  • $\begingroup$ (4) what relations and differences are between intuitionistic type theory and the second setting? Is the intuitioistic one based on first order logic, while the other on second or higher order logic? $\endgroup$
    – Tim
    Feb 25, 2012 at 13:37
  • $\begingroup$ (5) Wiki says lambda calculus is a formal system in mathematics logic, so I think it is a kind of logic different from the first, second or higher order logic, and therefore typed lambda calclulus is a kind of type theory different from intuitionistic type theory and the other one you mentioned? $\endgroup$
    – Tim
    Feb 25, 2012 at 16:14

You must log in to answer this question.

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