HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Introduction to type theory for a beginner?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
theorytypebeginnerforintroduction

Problem

I'm interested to read about type theory, but I'm quite a beginner. I know what sets are and how to work with them, but I don't have a deep understanding of set theory. I don't really understand the motivation behind type theory, other than that it was first developed to solve the problems with naive set theory.

I'm mainly interested in type theory because I heard it relates to proof theory (which I also don't understand well). I'm also not a mathematician or computer science by education.

Is there a good resource for beginners that introduces type theory, motivates it, shows how its different from set theory, why that's relevant, and shows how it can be used? I'd be satisfied if I have a thorough understanding of the general idea without understanding more advanced stuff.

Solution

Why has no one proposed Benjamin Pierce's Types and Programming Languages? That is a good introduction to type theory. Bob (Robert) Harper's Practical Foundations of Programming Languages is also a pretty good one.

Both of them introduce type theory from a computing perspective. If you like math better, try Rob Nederpelt and Herman Geuvers' Type Theory and Formal Proof: An Introduction. I have not taken a look at Basic Simple Type Theory by J. Roger Hindley yet, but I figure it should be good given the author (judging from the table of contents though, it looks hard).

Context

StackExchange Computer Science Q#85350, answer score: 4

Revisions (0)

No revisions yet.