Postscript
Looking Back
- 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 -------------------- ~ ---------------------------- software engineering mechanical/civil engineering
- inductively defined sets and relations
- inductive proofs
- proof objects
- Coq, an industrial-strength proof assistant
- functional core language
- core tactics
- automation
Looking Forward
- Logic Foundations (volume 1, by a set of authors
similar to this book's) continues on with this material
to introduce even more concepts in Coq, leading up to
some simple topics in programming language semantics.
- 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.
Other sources
- Other textbooks on discrete mathematics abound, and they
cover plenty of material we didn't discuss. There are also
whole fields of study surround set theory or
combinatorics---try taking such a class in the math
department!
- 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]. Real World Haskell, by Bryan - O'Sullivan, John Goerzen, and Don Stewart - [O'Sullivan 2008] ...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 \CITE{Chlipala - 2013}. Interactive Theorem Proving and Program - Development: Coq'Art: The Calculus of Inductive - Constructions, by Yves Bertot and Pierre Casteran - [Bertot 2004]. - 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
(* 2022-01-12 10:20 *)