My interest in the mathematical theory of computation is primarily due to the work of the brilliant logician Jean-Yves Girard on linear logic. Below is a (not very comprehensive) list of references for the parts of the theory of computation that I either know a little about, or am interested in. The books can generally be downloaded in PDF form from bookzz, but do buy a copy as well.

General “big picture” references on computation and logic:

- The Nature of Computation, a textbook by Cristopher Moore and Stephan Mertens.
- Towards a geometry of interaction by Jean-Yves Girard.
- The Blind Spot also by Girard, quite eclectic and unpolished, but full of interesting ideas (especially the sections on Russell’s paradox and complexity).
- Constructive mathematics and computer programming by Martin-Lof.
- Two puzzles about computation by Samson Abramsky.

Some references on lambda-calculus, System F and proof theory:

- Proofs and types by Jean-Yves Girard.

Some references on computational complexity theory:

- Why philosophers should care about computational complexity by Scott Aaronson.
- Topological views on computational complexity by Michael Freedman (Fields medallist and now director of Station Q).
- Light linear logic by Jean-Yves Girard.
- Light logic and polynomial time computation by Kazushige Terui.

Relations between computation and category theory:

- Lectures on the Curry-Howard isomorphism by Morten Heine Sorensen and Pawel Urzyczyn.
- Physics, Topology, Logic and Computation: A Rosetta Stone by John Baez and Mike Stay.
- Categorical semantics of linear logic by Paul-Andre Mellies.
- Notions of computation and monads by Eugenio Moggi.
- Homotopy type theory is a semantics of Martin-Lof type theory defined using homotopy-theory.

Relations between computation and physics:

- The Feynman lectures on computation, seminal work in the field of quantum computing, also has a good discussion of basics including Bennett’s work on irreversibility (find a PDF on bookzz).
- Complexity and phase transitions, Nature paper from 1999.
- There is a deep and interesting connection between Maxwell’s demon and topics in computation, for which see Szilard, Brillouin, Landauer and the papers of Bennett below.
- The thermodynamics of computation by Bennett 1982.
- Time-space tradeoffs for reversible computation by Bennett.

Some interesting videos:

- Lambda calculus, then and now by Dana Scott.
- Propositions as types by Philip Wadler.
- The future of programming by Bret Victor.