What do you think?
Rate this book
Program = Proof
This course provides a first introduction to the Curry-Howard correspondence between programs and proofs, from a theoretical programmer's perspective: we want to understand the theory behind logic and programming languages, but also to write concrete programs (in OCaml) and proofs (in Agda). After an introduction to functional programming languages, we present propositional logic, λ-calculus, the Curry-Howard correspondence, first-order logic, Agda, dependent types and homotopy type theory.
539 pages, Paperback
Published July 3, 2020
10 people are currently reading
103 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 2 of 2 reviews
February 19, 2022
One of the deepest ideas among all I have ever heard: a proposition is a type and proof is a program. This book explains how logic is connected to programming.
What is programming? It is writing proof. Simple and deep.
Find more cool ideas: https://stackoverflow.com/questions/2...
What is programming? It is writing proof. Simple and deep.
Find more cool ideas: https://stackoverflow.com/questions/2...
June 19, 2021
An excellent introduction the the Curry-Howard isomorphism. Additionally I found even the chapters who's material I was familiar with engaging and brought forward nice tidbits and perspectives that kept things engaging.
It is heavy on modern rule based notation which is nice especially sections of older material which were created before this style of notation became prominent (e.g. Natural Deduction).
Only slight downside is that there are a number of typos if that is something that bothers you. Apologies to the author, who specifically requested feedback on this, for not keeping track of these because I was deep into the book before I clued in that I should be keeping a list.
Overall its a great resource and very readable.
It is heavy on modern rule based notation which is nice especially sections of older material which were created before this style of notation became prominent (e.g. Natural Deduction).
Only slight downside is that there are a number of typos if that is something that bothers you. Apologies to the author, who specifically requested feedback on this, for not keeping track of these because I was deep into the book before I clued in that I should be keeping a list.
Overall its a great resource and very readable.
Displaying 1 - 2 of 2 reviews