9 ms·
Is it a good material to dive into this topic today?
by lugu 1y ago
Is it a good material to dive into this topic today?
- cjfd 1y agoSure, 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.
- avodonosov 1y agoHave you found this stuff useful during the many years since you learned it? Or you don't mean you mastered it enough to judge its usefulness?
- cjfd 1y agoI have a personal coq/rocq project regarding the verification of software so for that purpose it is highly useful. I also wrote a proof assistent myself (https://github.com/chrisd1977/system https://github.com/chrisd1977/system).
- quchen 1y agoTTOP 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).
- mogoh 1y agoTTOP? Do you mean TTFP?
- quchen 1y agoTAPL, I meant TAPL (Types and Programming languages by Pierce)! This would not have happened with a well-typed comment section. I mixed up OP's book (which is nice as well!) and the abbreviation. Sorry!
- deleted 1y ago[deleted]
- taolson 1y agoMiranda should still be readable for those with some Haskell background (it was a major influence on developing the Haskell language). I also have a more modern update to Miranda called Admiran: https://github.com/taolson/Admiran https://github.com/taolson/Admiran
- ks2048 1y agoA related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".
- 4ad 1y agoThey are very different books. TAPL is a book about programming language semantics, TTAFP is a programmer-oriented book about Martin-Löf type theory. There is very little overlap. TAPL is definitely the book to pick up if you are interested in programming language semantics. But if you are interested in logic, dependent types, Curry-Howard correspondence there are potentially better and more modern materials than TTAFP (not to say that TTAFP is bad). If you care about formalizing programs Sofware Foundations is a much better resource, and if you care about mathematics and logic, there are resources specifically suited to that.
- spewffs 1y agoWhat other books would you suggest? I've been reading TTAFP for a few months now and I don't like it very much. I was thinking maybe starting to read Principles of Dependent Type Theory by Angiuli and Gratzer but I'm not sure if it really covers the same area.
- lo_zamoyski 1y agoTAPL is a perfectly good book, but some in academia will tell you that it is somewhat dated.