How would I go about learning the underlying theory of the Coq proof assistant? I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use tactics to prove things like forall (n m : nat), n + n = m + m -&gt; n = m.
One place to start is  the Coq reference manual (pdf). Chapter 4 describes the underlying logic of Coq, and ultimately everything is based on this. It's called the calculus of (co)inductive constructions, and many  papers describe. Getting your hands on the Coq'Art book Interactive Theorem Proving and Program Development provides a more leisurely but not cheap introduction to Coq.

To learn about how tactics work, have a look at this earlier question: How do &#39;tactics&#39; work in proof assistants?

To build up the required theory, you need to learn about Type Theory. Most closely related to the theory underlying a proof assistant is probably Per Martin-Löf's Intutionistic Type Theory notes (or book) or the book Programming in Martin-Löf Type Theory, which is really about writing and proving theorems in type theory. A programming language perspective on type theory can be obtained from Pierce's Types and Programming Languages. Girard et al's Proofs and Types, which also addresses the importance of the Curry-Howard Correspondence, is another excellent reference.
Then you are probably well and truly ready to read Coquand and Huet's The Calculus of Constructions. Finally chase up some of the references in the back of the Coq manual.

There are other proof assistants, HOL, NuPRL, Mizar, Twelf, etc., and they have their theory too, so you can learn a lot too by reading in that direction.

Finally, for an overview of the history and future of proof assistants, check out the recent article by Herman Geuvers.