Learning type theory

I spent a very geeky Saturday reading about different kinds of logic programming languages, which somehow got me interested in learning more about type theory. After spending some time gathering introductory materials on my own I posted a question on /r/compsci asking for suggestions redditors might have on the subject. This page is both a collection of the suggested materials and general observations from /r/compsci denizens and some of my own musings on the subject; basically a learning diary of sorts. What that means is that

    1. Under no circumstances should you think I actually know what I'm talking about. I don't

    2. all corrections and further suggestions are more than welcome.

Prerequisites

It was suggested that it would be good to have some knowledge of at least the following areas before delving into type theory:

Some notes on the prerequisites

The connection between predicate calculus and lambda calculus was surprising, to say the least: it turns out that you can do computations using systems of formal logic. Take for example a function of type a

b which takes things of type a and gives you things of type b. When you think about it, succesfully applying that function proves that you can get something of type b from type a, so the type of the function is actually a proposition. The awesomeness doesn't end there: according to something called the Curry-Howard correspondence (C-H from now on), not only do types correspond to propositions, but whole systems of logic correspond to different lambda calculi. The upshot of this is that all programming language concepts have corresponding logical concepts: types correspond to propositions, recursion to induction and so on.

Structural induction seems to tie into C-H, since it can be used to prove some property P for all elements of a recursively defined type.

Out of all the prerequisites, operational semantics was the only one that was completely alien to me so I'll just quote Wikipedia's handy definition: "The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps". Its usage seems to be related to type checking: operational semantics can apparently be used to guarantee that an expression's type doesn't change during runtime. Couple this with strong typing and proper compile-time type checking and you have a language that shouldn't raise runtime type errors.

Free online materials covering the prerequisite topics

Since Wikipedia articles aren't always the best way to start learning something new, I dug up some introductory materials from various universities and institutions:

Note that some of the books and materials on type theory also cover the prerequisites.

Type theory

So far all I have regarding type theory is a few links. More to come once I actually get here.

Suggested books and online materials