3 ms·
I 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
by ionfish 16y ago
I 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/