Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
Congratulations: We've made it to the end!
(* ################################################################# *)
We've covered quite a bit of ground so far. Here's a quick review...
- Functional programming:
- "declarative" programming style (recursion over immutable data structures, rather than looping over mutable arrays or pointer structures)
- higher-order functions
- polymorphism
- Logic, the mathematical basis for software engineering:
logic calculus
- ------------------- ~ ----------------------------
- inductively defined sets and relations
- inductive proofs
- proof objects
- Coq, an industrial-strength proof assistant
- functional core language
- core tactics
- automation
(* ################################################################# *)
If what you've seen so far has whetted your interest, you have two
choices for further reading in the Software Foundations series:
- Programming Language Foundations (volume 2, by a set of
authors similar to this book's) covers material that
might be found in a graduate course on the theory of
programming languages, including Hoare logic, operational
semantics, and type systems.
- Verified Functional Algorithms (volume 3, by Andrew Appel) builds on the themes of functional programming and program verification in Coq, addressing a range of topics that might be found in a standard data structures course, with an eye to formal verification.
(* ################################################################# *)
Here are some other good places to learn more...
- This book includes some optional chapters covering topics
that you may find useful. Take a look at the table of contents and the chapter dependency diagram to find
them.
- For questions about Coq, the #coq area of Stack
Overflow (https://stackoverflow.com/questions/tagged/coq)
is an excellent community resource.
- Here are some great books on functional programming
- Learn You a Haskell for Great Good, by Miran Lipovaca Lipovaca 2011 (in Bib.v).
- Real World Haskell, by Bryan O'Sullivan, John Goerzen, and Don Stewart O'Sullivan 2008 (in Bib.v)
- ...and many other excellent books on Haskell, OCaml,
Scheme, Racket, Scala, F sharp, etc., etc.
- And some further resources for Coq:
- Certified Programming with Dependent Types, by Adam Chlipala Chlipala 2013 (in Bib.v).
- Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions, by Yves
Bertot and Pierre Casteran Bertot 2004 (in Bib.v).
- If you're interested in real-world applications of formal
verification to critical software, see the Postscript chapter
of Programming Language Foundations.
- For applications of Coq in building verified systems, the lectures and course materials for the 2017 DeepSpec Summer School are a great resource. https://deepspec.org/event/dsss17/index.html
(* Wed Jan 9 12:02:47 EST 2019 *)