Proofs and types
by Jean-Yves Girard · first published 1989
14mentions
6recommended by
10HN commenters
2010–2026first – last mentioned
55% recommend36% neutral9% critical
Why HN recommends it
A readable, idiosyncratic introduction to type theory and proofs, valued by readers who find Martin-Löf's writings hard going. Useful as a next step after basic logic for those wanting a more mathematical treatment.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
Mentions per year
What Hacker News says
Related books
2011–2022Certified Programming with Dependent Types
Adam Chlipala
Recommended by 25 · mentioned by 3125 recommend · 31 mention25 recommend · 3125 recommend
2008–2026Types and Programming Languages
Benjamin C. Pierce
Recommended by 132 · mentioned by 226132 recommend · 226 mention132 recommend · 226132 recommend
2007–2026How to Design Programs
Matthias Felleisen
Recommended by 277 · mentioned by 440277 recommend · 440 mention277 recommend · 440277 recommend
…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…
on “Why Lisp is a Big Hack (And Haskell is Doomed to Succeed)” ↗…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.
on “Untangling Mechanized Proofs” ↗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
on “Software Foundations by Benjamin Pierce et al.” ↗…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).
on “Ask HN: Which book can attract anyone towards your field of study?” ↗I strongly recommend "Proofs and Types" (http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html), which has the added advantage of being free.
on “Ask HN: any type theory book recommendation?” ↗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.…
on “Lively Linear Lisp – 'Look Ma, No Garbage' (1992)” ↗Some more food for thought on the meaning of =, from Girard's "Proofs and Types" [0]: > There is a standard procedure for multiplication, which yields for the inputs 27 and 37 the result 999. What can we say about that? A first attempt is to say that we have an equality "27 x 37…
on “For mathematicians, = does not mean equality” ↗Walk away now. Type Theory derailed my PhD studies. Seduced by constructivism, Curry-Howard, Martin-Löf and especially Girard's Proofs and Types, I wasted two years and subsequently abandoned my postgraduate studies. It's comp. sci. flavoured esoteric nonsense.
on “So you want to learn type theory” ↗…different in computer programs. I think it's important for computer scientists to understand this difference. Jean-Yves Girard, the inventor of system F in functional programming discusses this difference in Proofs and Types[1], in the very first section, called "Sense, Denotation and Semantics". [1]: http://www.paultaylor.eu/stable/prot.pdf
on “Why Don't Computer Scientists Learn Math? (2016)” ↗> Is there a source for that narrative? Girard mentions the connection with categories all the time. For example in "Proofs and Types" he proves various theorems along the lines of: the sub-category of coherence spaces and stable maps (one of the main models that LL was developed for) induced by some LL fragment is cartesian closed…
on “RZK: Experimental proof assistant for synthetic ∞-categories” ↗Yeah I think there’s some confusion here. When I hear “type theory” - I think Martin-Löf, Girard’s Proofs and Types, Curry-Howard, etc. Which is not a “theory of programming language types” - although the subjects are not completely isolated from each other. Then again, it’s been decades since I actually studied…
on “Why is it worth spending time on type theory? (2013)” ↗…approximations. I think that it is well accepted by now that "functional" is a spectrum, and one that includes Lisp. A short and nice discussion of this can be found in section 1.1 of Jean-Yves Girard's Proofs and Types[1]. I don't think anyone can accuse Girard of not knowing what functions and functional programming are. [1]: http://www.paultaylor.eu/stable/prot.pdf
on “Lisp is not functional (2010)” ↗It depends what you mean by "type theory", but you're right. See Pierce for a more practical introduction. "Proofs and Types" is more fundamental and focuses on the interplay between the operational semantics of the underlying language and the structure of its type system (read as proofs of properties of programs written in…
on “Ask HN: any type theory book recommendation?” ↗…sources but wikipedia is good too. * Proof trees - https://en.wikipedia.org/wiki/Method_of_analytic_tableaux * Constructive/Intuitionistic logic - https://en.wikipedia.org/wiki/Intuitionistic_logic * Proofs and Types - https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... * (In)completeness - https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... * Compactness - https://en.wikipedia.org/wiki/Compactness_theorem
on “Anatomy of a Lean proof for software engineers” ↗