I'm going through "Proofs and Types" and it's a wonderfully written book! First few chapters felt like a pleasure (especially for someone who already went through TAPL and TTFP, and had some experience with writing dependently typed code), but the ones on semantics, coherence spaces and the likes (namely, chapters 8, 12, and, to some extent, 9) feel quite over my current level.
So, a couple of questions:
- Is the presentation in the book relevant? I heard something about categorical interpretation, so not sure what's the current state of the art in this area.
- Is the subject itself relevant? Is this something that everyone wanting to understand type theory (and possibly eventually contribute to the research) knows, or is it rather a dedicated branch on its own?
- In any case, is there anything more accessible?