Okay, I just tried to read through the thing, and it looks much too difficult for what it’s trying to do. If anyone’s really interested in the topic, I’d recommend starting with something like the Wikipedia page for System F and assimilating more material as needed; that’ll certainly be easier for any programmer like me.
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).
I slogged through the first 30 pages. Section 2.2.1 “Interpretation of the rules” was surprisingly unclear. I could make sense of it only after using the Curry-Howard isomorphism given later on (because I’m already familiar with typed functional programming).
Section 3.3 on “arbitrary pluggings” and “variables and values as dual aspects of the same plugging phenomenon” is both informal and unclear.
I also didn’t see any definition of “abstraction”, “closed”, or “strictly simpler” in the corollary (p. 19) in section 3.4 on (head) normal form. “B strictly simpler (type) than A” probably means that A is built on top of B by one of:
A=B x X
A=X x B
A=B->X
A=X->B.
The material is either not self-contained, or out of order (I didn’t read the whole thing).
The book assumes a bit of familiarity with the subject and isn’t bureaucratic in formality. Many ideas are hard to present formally or aren’t even understood formally yet. I find the informal discussion in this book very valuable. It allows to see the motivation behind logic beyond text-crunching right from the beginning.
A closed term is one where all variables are bound (no free variables). Abstraction is a lambda-expression.
Okay, I just tried to read through the thing, and it looks much too difficult for what it’s trying to do. If anyone’s really interested in the topic, I’d recommend starting with something like the Wikipedia page for System F and assimilating more material as needed; that’ll certainly be easier for any programmer like me.
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).
If the goal is good understanding of “foundations” (however Girard himself may mock the concept), I see the book as being at just the right level.
I slogged through the first 30 pages. Section 2.2.1 “Interpretation of the rules” was surprisingly unclear. I could make sense of it only after using the Curry-Howard isomorphism given later on (because I’m already familiar with typed functional programming).
Section 3.3 on “arbitrary pluggings” and “variables and values as dual aspects of the same plugging phenomenon” is both informal and unclear.
I also didn’t see any definition of “abstraction”, “closed”, or “strictly simpler” in the corollary (p. 19) in section 3.4 on (head) normal form. “B strictly simpler (type) than A” probably means that A is built on top of B by one of:
A=B x X
A=X x B
A=B->X
A=X->B.
The material is either not self-contained, or out of order (I didn’t read the whole thing).
The book assumes a bit of familiarity with the subject and isn’t bureaucratic in formality. Many ideas are hard to present formally or aren’t even understood formally yet. I find the informal discussion in this book very valuable. It allows to see the motivation behind logic beyond text-crunching right from the beginning.
A closed term is one where all variables are bound (no free variables). Abstraction is a lambda-expression.