Resources for mathematicians hoping to learn more computer science

Question

Background:

I'm coming to the end of my masters degree in Mathematics and will be starting a PhD in Logic in August. The more logic I study, the more theoretical computer science I am exposed to, e.g. recursion theory, lambda calculus, but the underlying CS is brushed under the rug. My main areas of interest - set theory and category theory - also have applications in computer science, but so far I've only studied them from the point of view of pure mathematics.

Problem:

My lack of any computer science background sometimes makes it difficult to see the motivation or intuition behind what is going on, or how it could be applied. I get by, but I feel like it would be healthier to branch out a little bit... it occurs to me that, for the benefit of my future research, I should learn some computer science.

Most CS books I've looked at haven't been very suitable for my purposes, either being too basic and untechnical, or presupposing the kind of CS background that I don't have. They seem to be aimed at people who are quite computer-savvy but who have little in the way in mathematical background - my situation is the opposite.

Question:

What books or other resources are there which could help a mathematician-turned-logician in their goal of gaining a working knowledge of (theoretical) computer science?

I'm looking for something more wholesome than a few seminar talks and more in-depth than The New Turing Omnibus, but I don't have the time or resources to do another undergraduate degree. (It may be that I'm asking for something that doesn't exist.)

Sorry if the question is too vague or ill-posed. I felt it was more suitable here than on MSE but I'll be happy to migrate it if needs be.

Answer 1

You're essentially asking for resources that will let you turn your existing knowledge of logic, recursion theory, and category theory into knowledge about theoretical computer science.I would suggest looking at realizability theory, especially via its connections to topos theory and categorical proof theory.

Here are a handful of suggestions; my advice is to pick one and go into depth. With the exception of Taylor's book (which explains this), my suggestions assume you have been exposed to enough lambda calculus and category theory to have seen categorical interpretations of the simply-typed lambda calculus.

• Paul Taylor's book Practical Foundations of Mathematics

  IMO, this is probably the single best technical introduction to the relationship between logic, category theory and computation. It assumes almost no pre-requisites, but it gets into quite deep waters very quickly, and is sure to tax (and greatly improve) your mathematical maturity.

• Wesley Phoa's notes An Introduction to Fibrations, Topos Theory, the Effective Topos, and Modest Sets

  These are some lecture notes that Wesley Phoa wrote up. If you are categorically fluent, then these notes offer a really fast path into understanding some of the most important constructions in realizability and topos theory (namely, the construction of the effective topos).

• Bart Jacobs' book Categorical Logic and Type Theory

  This is one of the definitive references on the categorical semantics of type theory. It is also very large.

At the same time you are reading one of these books, I would advise downloading and learn how to use the Agda programming language. This language implements the sophisticated type theories described above, and IMO it is incredibly helpful to see how the often quite subtle semantic constructions cash out in type theory.

Andrej Bauer can probably give you even better advice. Perhaps he can be persuaded to post. :)

Answer 2

The two books that come to mind are

Introduction to the Theory of Computation by Sipser

and

Introduction to Algorithms by Cormen et al.

I agree with usul who said that theoretical computer science is a broad area and we could give better references if you were more specific about what you want to learn.