COMP 360-1: Computer-Checked Programs and Proofs

Office Hours

Tuesday, noon to 1pm and Wednesday, 11am-noon and by appointment


We will use Piazza for questions about the assignments, for students to discuss course materials, and to make announcements about the class. You are responsible for being current with the information and discussions that are posted there.

You will get an email from Piazza with a link inviting you to create an account within the first week of the term. If you haven't gotten one in that time, please contact course staff.

In addition to the web interface, there are Piazza apps for Android and iOS available for free through their respective app stores.

Getting Agda

Please try to install Agda version, which is the latest stable release, but the course materials will likely work with other recent versions (2.3.2, the development version from darcs) if for some reason those are easier to install. We recommend trying to install Agda according to the following directions:
  1. Install the Haskell Platform. The latest version, 2013.2.0.0, will definitely work for Agda, though other versions may also work. This is available for Windows, Mac OS, and Linux.
  2. Use cabal to install Agda.
    1. Run cabal update to get the latest package list.
    2. Run cabal install Agda. This will install a bunch of libraries that Agda depends on, and then Agda itself.
    3. Add $HOME/Library/Haskell/bin (on a Mac) or $HOME/.cabal/bin (on Linux) or ? (on Windows) to your path, so that the executables installed by cabal are in your path.
    4. When you're done, you should be able to do
      % agda --version
      Agda version
  3. Install some version of emacs, if you don't already have it. On a Mac, I use Carbon Emacs, but Aquamacs should also work.
  4. Run agda-mode setup to add Agda to your emacs configuration. If, for some, reason agda-mode setup fails, you can add the following lines to your .emacs manually:
    (load-file (let ((coding-system-for-read 'utf-8))
                    (shell-command-to-string "agda-mode locate")))

If that fails, more information is available here. For Agda, there are some pre-built packages for linux distributions, but do not use the Windows installer (it is out of date), and there is no pre-built package for Mac. If you do not install Haskell using the Haskell Platform, then watch out for this performance issue with the hashtable package: make sure you get hashtable version 1.1.2.x (the Haskell Platform has an appropriate version).

Issues and workarounds:

GNU emacs

The guiding principle of emacs philosophy is that you should never have to leave emacs to preform a task if you don't want to. If you're writing C, it can run your makefile, and show you GDB output internally. It even has tetris and email clients built in. Despite being extremely large in this sense, emacs scales down to the smallest of text files elegantly.

The most sane version to use is GNU emacs, although both GNU emacs and Xemacs are installed on the Andrew UNIX machines. There's a ton of good documentation for how to use it available on the web, some of which is linked here.


If we have written assignments, you may wish to use LaTeX.

LaTeX is built from Don Knuth's TeX typesetting language, and has grown through community support to be both extremely powerful and easy to use. LaTeX is installed on the Andrew UNIX servers, and can be downloaded and installed on local machines as well. There are any number of excellent resources about how to use LaTeX; a few are listed here for your convenience.

LaTeX source files can be created with any text editor, so emacs and vim are excellent choices. There are several LaTeX specific IDEs that you may find more comfortable to use, depending on your working environment:

Valid CSS! Valid XHTML 1.0 Strict