What do you think?
Rate this book
Software Foundations
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant.
The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity is helpful. A one-semester course can expect to cover Logical Foundations plus most of Programming Language Foundations or Verified Functional Algorithms, or selections from both.
The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant.
The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity is helpful. A one-semester course can expect to cover Logical Foundations plus most of Programming Language Foundations or Verified Functional Algorithms, or selections from both.
800 pages, ebook
First published June 28, 2011
25 people are currently reading
330 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 - 3 of 3 reviews
March 14, 2012
After I managed to get over the hurdle of starting this book (I needed some serious math refreshing), it quickly became one of my favorite books. Programming in Coq is extremely addictive, and Software Foundation's treatment of it and of programming languages concepts in general are very well done.
Additionally, I think it's worth pointing out that I would have loved to have learned proofs and induction in this style (proofs as programs) rather than my dry boring university lectures from the math department with pencil and paper proofs. Though, as they say several times in the book, make sure you can still do the pencil and paper proofs, because Coq has a way of lulling you into places where you have absolutely no idea what's actually going on in your proof. Sketch your ideas for your proofs before you code them up.
Additionally, I think it's worth pointing out that I would have loved to have learned proofs and induction in this style (proofs as programs) rather than my dry boring university lectures from the math department with pencil and paper proofs. Though, as they say several times in the book, make sure you can still do the pencil and paper proofs, because Coq has a way of lulling you into places where you have absolutely no idea what's actually going on in your proof. Sketch your ideas for your proofs before you code them up.
September 25, 2013
The best introduction on using dependently typed progamming to prove a lot of fundamental CS. Begins from simple logic all the way to partial evaluation in lambda calculus.
The problem sets are really fun! All exercises are in Coq, feel like you're solving a puzzle game.
The problem sets are really fun! All exercises are in Coq, feel like you're solving a puzzle game.
April 5, 2020
The exercises are really hard and it is not always kept up to date with the most recent Coq version (8.11 as I am writing this)
Displaying 1 - 3 of 3 reviews