This appears to be a new edition/refactoring/redesign of the previous version of Software Foundations. I haven't had much time to look through it but it looks like there is new material (volume 3?) (EDIT: found a hosted copy of the old version, at least for now: https://softwarefoundations.cis.upenn.edu/current/toc.html)
This book is very good for self-study. It teaches you Coq, a formal proof assistant/language. Formally-verified programs can be extracted from these proofs into languages like Haskell and OCaml.
1 comment
[ 1.5 ms ] story [ 13.6 ms ] threadThe previous version was hosted at http://www.cis.upenn.edu/~bcpierce/sf which now redirects to here.
---
This book is very good for self-study. It teaches you Coq, a formal proof assistant/language. Formally-verified programs can be extracted from these proofs into languages like Haskell and OCaml.