References on computation

Mon, Oct 26, 2015

My interest in the mathematical theory of computation is primarily due to the work of the logician Jean-Yves Girard on linear logic. Below is a list of references for the parts of the theory of computation that I either know a little about, or am interested in.

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.
• 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.