3 ms·
By the way, I am currently doing a literature study into type theory for my study and I was annoyed by the lack of introduction material for programmers wanting
by merijnv 16y ago
By the way, I am currently doing a literature study into type theory for my study and I was annoyed by the lack of introduction material for programmers wanting to learn more about it. I've been thinking of writing a "Type theory from first principles for dummies" but I was unsure how much interest there'd be in something like that. If you (or other people here on HN) would be interested in that let me know...
- ionfish 16y agoI think that would be a very valuable article. Right now people are basically stuck with TAPL [1], which (while being a fantastic book) is pretty meaty and not exactly cheap. I've been examining the type theory literature myself over the last couple of months (admittedly more from a mathematical angle than a programming one), and there is definitely a dearth of good introductory material. Girard's Proofs and Types is a great book, but it's not easy going and doesn't have a huge amount of direct relevance to programmers. In case anyone else is interested (merijnv, I assume you've glanced at all of these) I have a small bibliography of type theory books [2]. [1] http://www.cis.upenn.edu/~bcpierce/tapl/ http://www.cis.upenn.edu/~bcpierce/tapl/ [2] https://gist.github.com/716834 https://gist.github.com/716834
- stralep 16y agoI'm also currently interested in this area, and I would recommend Interactive Theorem Proving and Program Development. At the same time, it is practical and theoretical. http://www.labri.fr/perso/casteran/CoqArt/index.html http://www.labri.fr/perso/casteran/CoqArt/index.html
- primodemus 16y agoBenjamin Pierce has a course on the mathematical theory of programming languages, using the Coq Proof Assistant: http://www.cis.upenn.edu/~bcpierce/sf/toc.html http://www.cis.upenn.edu/~bcpierce/sf/toc.html Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
- agentcoops 16y agoThese papers by Luca Cardelli are quite good: http://lucacardelli.name/Papers/TypeSystems.pdf http://lucacardelli.name/Papers/TypeSystems.pdf http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf