It’s a great book, but in my experience, it’s more useful as a motivator than as a source of information. That is, after reading Girard’s cryptic and tantalizing off-hand remarks, you are dying to know what on earth he is talking about.
I think part of the reason is that the book is based on notes from a series of lectures Girard gave; in my experience oral lectures tend to be a lot more sketchy than things which are written down (others disagree...). The other part of the reason is that this is Girard. :)
For readers who are new to lambda calculus or proof theory but are interested to learn, I’d recommend supplementing it with a gentler text like Sørensen and Urzyczyn’s Lectures on the Curry-Howard Isomorphism (book, shorter free online version), which contains actual explanations. The first few chapters of this covers the same material as the first few chapters of Girard’s book. (They diverge a bit towards the end).
It depends on your background. I read a lot on program semantics before opening this book, but never systematically on logic. It was genuinely helpful (and counting—I haven’t finished it yet).
It’s a great book, but in my experience, it’s more useful as a motivator than as a source of information. That is, after reading Girard’s cryptic and tantalizing off-hand remarks, you are dying to know what on earth he is talking about.
I think part of the reason is that the book is based on notes from a series of lectures Girard gave; in my experience oral lectures tend to be a lot more sketchy than things which are written down (others disagree...). The other part of the reason is that this is Girard. :)
For readers who are new to lambda calculus or proof theory but are interested to learn, I’d recommend supplementing it with a gentler text like Sørensen and Urzyczyn’s Lectures on the Curry-Howard Isomorphism (book, shorter free online version), which contains actual explanations. The first few chapters of this covers the same material as the first few chapters of Girard’s book. (They diverge a bit towards the end).
It depends on your background. I read a lot on program semantics before opening this book, but never systematically on logic. It was genuinely helpful (and counting—I haven’t finished it yet).