COMP 360C: Computer-Checked Programs and Proofs

Office Hours

Tess Lepeska-True: Sunday, 3:30-5pm, Exley 72
Dan Licata: Tuesday, 4:10-5pm, Olin 14 or Exley 633
Zameen Cater: Tuesday, 7:30pm-9pm, Exley 113
Dan Licata: Wednesday, 2:50pm-4:30pm, Exley 137
Adam Kleber: Wednesday, 7:30pm-9pm, Exley 113

Readings

It should be possible to do the assignments using only the material covered in lecture and the readings linked from the lectures page. However, here are some optional additional readings that you might find useful:

• Documentation on the Agda Wiki
• A book on formalizing programming languages in Agda by Wadler, Kokke, and Siek. Note: we will not be covering much programming language metatheory in this class, but Part 1 might be useful.
• Tutorial by Norell/Chapman. Warning: syntax may be out of date, but this is one of the original sources.
• Another early Tutorial, by Bove/Dybjer

Getting Agda

VSCode

1. Install VSCode. Note: if you have a previous installation, you may need to update it; the Agda mode has problems on version 1.92 but works OK on 1.97 and 1.108.
2. Click on the extensions icon on the left-hand toolbar, and install agda-mode (agda-mode on vscode), Ting-Gian LUA
3. Create a new file test.agda.
4. In the search/command bar at the top of the screen, type

   >Agda: Load

   to load your empty test file.
5. This should generate a popup asking if you want to install the Agda Language Server. Install it.
6. Now do >Agda: Load again and you should see an Agda output at the bottom with the message All Done.

Emacs

1. Install Agda version 2.8.0 from a github release by downloading one of these pre-compiled versions and storing it somewhere on your computer:
• Mac M1, M2, M3, M4, M5 processor
• Mac with Intel processor
• Windows
• Linux
2. Put the above executable in your PATH. How to do this depends on your Terminal's shell. In BASH you can do

             echo 'export PATH="placeyouputagdainthepreviousstep:${PATH}"' >> ~/.bash_profile
           

3. On newer versions of MacOS, you will need to convince MacOS to run Agda, even though it's a random executable you downloaded from the Internet. To do this, try to run Agda by typing agda in the Terminal, and let the OS block it. Then go to your Mac Settings/Privacy and Security, scroll down until you see Agda, and then click Allow. Try to run Agda again, and you should get an option to override the security protections and run it. Do that, and then MacOS will let you run it from now on.
4. If you have Linux, you almost certainly have emacs installed. For Mac and Windows get:
   • GNU emacs for Mac OS.
   • GNU emacs for Windows
5. Follow the Installation instructions for agda-mode, which is how emacs talks to Agda.
6. Some emacs resources:
   • Start with this tutorial on getting started with emacs
   • To exit emacs, type Control-X, then Control-C. A prompt may appear asking you about saving any changes you made; if this happens, you will need to answer it before exiting.
   • The emacs wiki is the omnibus resource for emacs usage
   • Wikipedia has an article on the general history and culture of emacs, for the curious.