6.8

7 Resources

The resources listed on this page are not required for the course, or likely to be of much use in fulfilling course requirements, but they may be of interest to those wishing to learn more.

You should not be looking for the solutions to assignment questions online, but for more information on related topics beyond the scope of the course, I would recommend the Stanford Encyclopedia of Philosophy instead of Wikipedia. The SEP has articles written, reviewed, and edited by expert professionals.

Philip Wadler’s papers "Propositions as Types" and "Proofs are Programs" are very readable overviews of the ideas behind the Curry-Howard correspondence and their consequences (and his talks on the subject are very watchable, if you have the time).

The paper "The Road To Modern Logic - An Interpretation", by Jose Ferreiros (Bulletin of Symbolic Logic, 7:4, pp. 441-484, 2001) is a very detailed study of the historic development of first-order logic. It is available online through the UW Library.

The Coq and Agda Web pages are good starting points for learning more about these proof assistants. There are several good books using Coq, including the entirely online Software Foundations, which is the textbook I used for CS 798 in Fall 2016, and to which I have contributed.

Herman Geuvers offers a nice overview of these and many other systems in his 2009 paper "Proof assistants: history, ideas, and future".

Idris is a programming language with Haskell-like syntax and full support for dependent types. Its designer wants it to be used for programs that are actually run, not just compiled! There is a book in progress.

A recent development worth keeping an eye on is Lean, a state-of-the-art proof assistant created by Microsoft Research and CMU. The online tutorial is quite well written, and runs a version of the software compiled to Javascript in your browser, making it very easy to take a quick look (no manual installation required).

David Turner, the designer of Miranda (the first practical lazy functional programming language, and a major inspiration for Haskell) has a nice paper titled "Total Functional Programming" which points out many drawbacks of the common practice of allowing partial functions, even for systems that are not being used for proof.

I host Brad Lushman’s version of my CS 245 slides from 2007 for those who want a look at a more conventional approach to logic and computation.