Is it a good material to dive into this topic today?
cjfd•5m ago
Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing rules' in the coq (nowadays rocq) manual. That is a 'slightly' higher friction way of learning this stuff. This document seems to be more pedagogical.
quchen•2m ago
TTOP is the standard work on the topic. Some parts I would say fell out of fashion (using Miranda for example), but many parts are either timeless or still just as relevant.
That said, the book is very dense; for me it was just too much the first time I tried to read it. After circling back to it after a while it gets much easier, because you know what parts you really need (which is a common pattern for me at least with everything academic).
lugu•1h ago
cjfd•5m ago
quchen•2m ago
That said, the book is very dense; for me it was just too much the first time I tried to read it. After circling back to it after a while it gets much easier, because you know what parts you really need (which is a common pattern for me at least with everything academic).