COMP 360-1: Computer-Checked Programs and Proofs

Office Hours

Dan: Thursday, 2:30pm-3:30pm, Exley 633
Joomy: Monday, 7pm-8:30p, Exley 109
Max: Wednesday, 7pm-8:30p, Exley 137


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

  1. Install the Haskell programming language.
    • On a Mac, you can install Haskell for Mac OS X. If you have El Capitain, get GHC 10.7.1, and then follow the instructions at the above link (the GHC 10.7.2 version seems to have some problems with the new Mac OS).
    • On Windows or Linux, install the Haskell Platform.
  2. With Haskell, you should get the cabal tool for installing Haskell packages Use cabal to install Agda.
    1. You may need to add this to your path if the Haskell installer doesn't successfully do it. On a Mac, it will probably be in /Applications/
    2. Run cabal update to get the latest package list.
    3. Run cabal install Agda. This will install a bunch of libraries that Agda depends on, and then Agda itself. If you get an error about missing happy or alex, type cabal install happy or cabal install alex.
    4. When you're done, you should be able to do
      % agda --version
      Agda version 2.4.2.x
      If the cabal install agda finished but this doesn't work, that means your cabal-installed executables are not in your path.
  3. Install some version of emacs, if you don't already have it (see the directions below). 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")))

Issues and workarounds:

Text Editors


If you have Linux, you almost certainly have emacs installed. For Mac and Windows get:

Some emacs resources: