Comment Comment by nextos Try http://adam.chlipala.net/frap/It's a really great book as an introduction to semantics and proofs.A great alternative is http://www.concrete-semantics.org/.Concrete Semantics uses Isabelle, which is based on ZFC set theory. Whereas FRAP uses Coq, that employs constructive types.https://softwarefoundations.cis.upenn.edu is also fantastic, covers some of the same topics, and proceeds a bit more slowly.I'm betting formal methods will become more wildly used in the 2020s. It'd be interesting to see e.g. reinforcement learning used to automate proof discovery. parent nextos 6 years ago
It's a really great book as an introduction to semantics and proofs.
A great alternative is http://www.concrete-semantics.org/.
Concrete Semantics uses Isabelle, which is based on ZFC set theory. Whereas FRAP uses Coq, that employs constructive types.
https://softwarefoundations.cis.upenn.edu is also fantastic, covers some of the same topics, and proceeds a bit more slowly.
I'm betting formal methods will become more wildly used in the 2020s. It'd be interesting to see e.g. reinforcement learning used to automate proof discovery.