Book:

• Additional exercises, a monotonically growing set. This document also addresses technical errors in the text through exercises, thus serving as a form of errata. So far, we've identified the errors; but if you find one, we'll be grateful and acknowledge you in the resulting exercise.
• A list of errors.
• πVC: The Pi Verifying Compiler.
• You may have access, if your university has subscribed, to an electronic version through SpringerLink.