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.
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.