Resources

Text books

A number of excellent books and on-line resources overlap with the course's content and can provide alternate explanations despite differences in notation and approach. Let the instructor know if you have trouble finding the intersection between these resources and the course content.

• "Types and Programming Languages" by Benjamin C. Pierce, MIT Press, 2002.
  Available on reserve at the library.
• "Software Foundations" by Benjamin C. Pierce et al., Volume 1: Logical Foundations and Volume 2: Programming Language Foundations.
  Available as literate Coq files.
  Also available as an interactive web-based version.
  Also available as literate Agda files thanks to Philip Wadler, Wen Kokke and Jeremy Siek.
• "Program Proofs" by Rustan Leino, MIT Press, 2023.
• "Programming Languages: Build, Prove, and Compare" by Norman Ramsey, Cambridge University Press, 2022.
• "Practical Foundations for Programming Languages" by Robert Harper, Cambridge University Press, 2013.
  Draft available on Harper's website.
• "Concepts in Programming Languages" by John C. Mitchell, Cambridge University Press, 2003.
  Available online through Harvard University Libraries eContent Collection.
• "The Formal Semantics of Programming Languages" by Glynn Winskel, MIT Press, 1993.
  Available on reserve at the library.
• "Programming Languages: Application and Interpretation" by Shriram Krishnamurthi.
  There are two editions, both available on the author's website: http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/.

OCaml resources

• Installation: https://ocaml.org/docs/install.html
• Tools: https://github.com/realworldocaml/book/wiki/Installation-Instructions

  This link gives instructions for installing things like Tuareg (a useful emacs mode) and Merlin (advanced IDE features).

  Installing Tuareg is pretty simple and will make your OCaml coding experience a lot nicer (though it's of course not necessary). Merlin is probably overkill unless you know what you're doing.

• Learning:
  • Standard library documentation: http://caml.inria.fr/pub/docs/manual-ocaml/libref/index.html
    The following documentation may be particularly useful as you work on your assignments.
    • Sets: http://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.Make.html
    • Maps: http://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.Make.html
  • Everything you need to know and more: http://caml.inria.fr/pub/docs/manual-ocaml/index.html
  • Code examples: http://ocaml.org/learn/tutorials/99problems.html

See also the CS51 Resources web page for OCaml books, references, and tutorials.

Coq resources

• Download Coq.
• Coq includes an IDE, CoqIDE. Alternatively, with Emacs, you can use Proof General.
• Coq documentation.

Dafny resources

• Dafny on Github.

Haskell resources

• Download The Haskell Platform.
• List of Haskell tutorials. If you want to get more meta, see How to Learn Haskell.
• haskell.org contains lots of reference information, language specification, etc.