Proofs and types

What Hacker News says

1. amateurlogicianMar 2022
   Girard's rhetoric never fails to keep me hooked. I treasure any number of works of Girard, whether his introductions to Type Theory and his Linear Logic or notes on his quest for Transcendental Logic. Clear prose of exposition, to the point and clearly motivated, intermingled with literary allusions in critique of philosophers' ideas of truth, the work of Girard is truly a gem.

   Particularly entertaining is his 'A pure waste of paper' (Appendix A of 'LOCUS SOLUM') (https://girard.perso.math.cnrs.fr/0.pdf). I could flip to a random page of his 'appendix' and just sink in.

   A fine introductory work of his to the subject would be 'PROOFS AND TYPES' (https://people.mpi-sws.org/~dreyer/ats/papers/girard.pdf).

   Show morethread
2. nextosNov 2020
   A similar book to Concrete Semantics, which I love, is Formal Reasoning about Programs by the same group the OP link comes from: http://adam.chlipala.net/frap/frap_book.pdf

   ML for the Working Programmer is written by Paulson, one of the main persons behind Isabelle, and ends up with a prover project: https://www.cl.cam.ac.uk/~lp15/MLbook/

   Paulson teaches an undergrad course in Cambridge which is now using Huth & Ryan as a textbook. It's an incredible book that focuses on logic, SAT solvers and model checking. Probably the place to begin. An incomplete draft 2nd edition is in the authors website: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/tmp/Anongporn/Ch1+3.pdf

   If you are interested in tableaux techniques, First-order Logic and Automated Theorem Proving by Fitting is a good text.

   Personally, I think the place to start from is Huth & Ryan. Logic is the calculus of CS. Then progress to type theory using a book like TAPL by Pierce or Proofs and Types by Girard.

   Then, depending on your interests, you can proceed to model checking, program analysis and theorem proving. For the first two, the classics are Katoen and Nielson & Nielson, respectively.

   Show morethread
3. derrizJul 2019
   I remember really liking his book Proofs and Types which was a revelation after struggling with Martin-Löf’s writings.

   One outcome of that attention was a nice and blazingly fast for an FPL called Clean which offered a more modern Haskell/MLish syntax. Actually came across this previous discussion while searching for a link: https://news.ycombinator.com/item?id=15937597

   thread
4. mafribeDec 2015
   What's a suitable resource depends on your background. If you like books, "Proofs and Types" by Girard, Lafont, Taylor [1] is a great read, albeit idiosyncratic.

   [1] http://www.paultaylor.eu/stable/prot.pdf

   thread
5. ionfishJan 2011
   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/

   [2] https://gist.github.com/716834

   Show morethread
6. tomstuartMar 2010
   I strongly recommend "Proofs and Types" (http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html), which has the added advantage of being free.
   thread