This website is out of date, please refer to the site on github.

Learn Type Theory

Posted on August 14, 2015
Tags: types

I’ve been trying to write a blog post to this effect for a while now, hopefully this one will stick. I intend for this to be a bit more open-ended than most of my other posts, if you’re interested in seeing the updated version look here. Pull requests/issues are more than welcome on the repository. I hope you learn something from this.

Lots of people seem curious about type theory but it’s not at all clear how to go from no math background to understanding “Homotopical Patch Theory” or whatever the latest cool paper is. In this repository I’ve gathered links to some of the resources I’ve personally found helpful.

Reading Advice

I strongly urge you to start by reading one or more of the textbooks immediately below. They give a nice self-contained introduction and a foundation for understanding the papers that follow. Don’t get hung up on any particular thing, it’s always easier to skim the first time and read closely on a second pass.

The Resources


Proof Assistants

One of the fun parts of taking in an interest in type theory is that you get all sorts of fun new programming languages to play with. Some major proof assistants are

Type Theory

Proof Theory

Category Theory

Learning category theory is necessary to understand some parts of type theory. If you decide to study categorical semantics, realizability, or domain theory eventually you’ll have to buckledown and learn a little at least. It’s actually really cool math so no harm done!

Other Goodness

comments powered by Disqus