Type Theory and Formal Proof
by Rob Nederpelt, Herman Geuvers · first published 2014
85% recommend15% neutral
Why HN recommends it
Gradual, mathematically presented introduction to type theory, from untyped lambda calculus up to dependent types and formal proof; recommended for beginners and those interested in proof assistants.
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
2014–2025Type theory and functional programming
Simon Thompson
Recommended by 2 · mentioned by 52 recommend · 5 mention2 recommend · 52 recommend
Intuitionistic type theory
Per Martin-Löf
Recommended by 1 · mentioned by 51 recommend · 5 mention1 recommend · 51 recommend
2007–2026How to prove it
Daniel J. Velleman
Recommended by 78 · mentioned by 10478 recommend · 104 mention78 recommend · 10478 recommend
2008–2026Elements
Euclid
Recommended by 60 · mentioned by 22560 recommend · 225 mention60 recommend · 22560 recommend
2008–2026Types and Programming Languages
Benjamin C. Pierce
Recommended by 132 · mentioned by 226132 recommend · 226 mention132 recommend · 226132 recommend
2015–2026Deep Work
Cal Newport
Recommended by 310 · mentioned by 498310 recommend · 498 mention310 recommend · 498310 recommend
2007–2026How to Design Programs
Matthias Felleisen
Recommended by 277 · mentioned by 440277 recommend · 440 mention277 recommend · 440277 recommend
I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university…
on “Counterexamples in Type Systems” ↗…from logicians) are actually quite straightforward, and the papers are not necessarily conceptually difficult so much as layered in their use of abstraction. I'll mention that Nederpelt and Geuvers' Type Theory and Formal Proof: An Introduction was recommended to me for this topic. I haven't had a chance to study it yet, but I'd say it's worth checking out.
on “Functional Algorithms, Verified” ↗Books. Some books on my shelf covering these topics: "Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search) First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof "Computation and Reasoning: A Type Theory…
on “Why is it worth spending time on type theory? (2013)” ↗I've got interested in formalization of mathematics recently and found the book Type Theory and Formal Proof by Nederpelt and Geuvers is a really nice one, taking you from the untyped lambda calculus and gradually extending the type system until you get the full dependent type theory and the Calculus of Constructions…
on “The Lambda Calculus (2023)” ↗…it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels... If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is…
on “Bend – a language that blocks AI mistakes via proof and runs on GPUs” ↗…pattern of using state of the art work in two different areas (LLMs and theorem proving) absolutely has the potentially to fundamentally change how mathematics is done. There's a great picture on pp 381 of Type Theory and Formal Proof where you can easily see how LLMs can be placed in two of the most tricky parts of that diagram to solve. Because the work is formally verified we can throw out entire classes of LLM problems (like hallucinations).…
on “AI solves Erdos problem #728 (Terence Tao mathstodon post)” ↗Tangential book recommendation: I have found the first chapters of "Type Theory and Formal Proof" a great in-depth introduction into lambda calculus and its typed variations.
on “Whiteboard problems in pure Lambda Calculus” ↗Type Theory and Formal Proof: An Introduction A ground up walk-through for using dependent types for formal proof. What I liked about this book is that it's presented more as mathematics than as computer science: you can work through…
on “Ask HN: Do you recall any book or course that made a topic finally click?” ↗I learnt it from "Type Theory and Formal Proof" when I wanted to understand type theory (I was in a community of functional programmers). BTW, nice book, I always recommend it to absolute beginners.
on “A λ-calculus interpreter written in C preprocessor macros” ↗Type Theory and Formal Proof is one of the better books I've found. It starts with untyped lambda calculus and works up to a dependently typed proof calculus in gradual steps. So if you are looking for a book then that's one of the…
on “Ask HN: What are you currently learning?” ↗Type Theory and Formal Proof (https://www.cambridge.org/core/books/type-theory-and-formal-...)
on “Ask HN: What's the "best" book you've ever read?” ↗What's interesting about this view is that theorem provers ultimately boil down to sufficiently advanced type checking (the book Type Theory and Formal Proof is an excellent overview of this topic). Literally the heart of proof assistants like Lean is "if it compiles, you've proved it". So more practical type systems can be viewed as "little" theorem provers…
on “To be a better programmer, write little proofs in your head” ↗…advanced type system, you could, in fact, prove more sophisticated things about the performance of your code (for example that the shapes of all your matrices matched). A great book on this topic is Type Theory and Formal Proof [1]. 0. https://lean-lang.org/functional_programming_in_lean/ 1. https://www.cambridge.org/core/books/type-theory-and-formal-...
on “Project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover” ↗What; Nederpelt - Type theory and formal proof Why; formal verification is a hobby of mine and and I read the article about how to improve my brain (one of them being basically kicking it harder with new things to learn) so I decided to plough through…
on “Ask HN: What are you reading? (July 2016)” ↗…ideas about how I want it to be, but the language seems like the hardest part of the "project", by far I would say. Having finished intro books on logic, automata and category theory, I am now starting "Type Theory and Formal Proof" and writing a general purpose parser. Even if I end up, for whatever reason, abandoning it before doing anything, the journey is definitely worth it.
on “OMU – “One Man Unix”” ↗