1. windless
  2. snu-sf



Software Foundations 2014 Fall @ SNU

Instructor: Gil Hur (gil dot hur at sf dot snu dot ac dot kr)

TA: Jeehoon Kang (574ta at sf dot snu dot ac dot kr)

  • Office hour: Mon/Wed 15:00-16:00 Rm 312-2 Bldg 302
  • The previous TA mail address works, but please use the new one if possible :)


  • HW 7's due is delayed for 1 week.
  • Submission status for homework's will be posted here; stay tuned!
  • Exercises with 5 stars are ``challenge'' problems; you don't have to solve, but encouraged to solve.
  • If you have any question, ask in the issue tracker in the repository.
    • Email TA for personal matters, please.
  • READ CAREFULLY this instruction. Especially, give attention to the Homework section.


  • Honor code: do not copy other's source code, including other students' and resources around the Web. Especially, do not consult with public repositories on software foundations. DO NOT CHEAT.

    • Exception: you can ask question in the issue tracker with your code paste ;-)
  • Use designated versions of software in this class to avoid version incompatibility. Your submission will not be properly graded if you do not follow this instruction. Use Coq 8.4pl4. Download software foundations as mentioned below.

  • Maintain a Git repository for homework.

    • Fork the skeleton by clicking it.
      • To do this, you have to register Bitbucket.
      • Your repository should be private for hiding from other students. Check This is a private repository at Access Level.
    • Invite TA to your private repository. TA's Bitbucket account is windless.
    • Register your information here.
    • TA will download your repository at the homework due, and grade based on the downloaded repository's master branch at the time.
  • Your repository should be well compiled.

    • TA will compile by make clean; make in Linux environment. This should not fail.
  • Fill in (* FILL IN HERE *) in Coq files.

    • Do not change otherwise. Especially, do not change the given definition, if not so directed; do not change Makefile; etc.
    • Exercises not related to formal proof will not be scored. For example, you are not required to do "informal proof" and "explanation" for score. But I recommend you to do those questions, too, anyway (for your own good!)
    • For those exercises that require you to write down the statement of lemmas, please do those exercises. (Omitting these kinds of exercise would severely restrict boundary, I think).
  • Homeworks:

HW Number Files Due
1 Basics.v 2014/09/17 09:30
2 Induction.v 2014/09/24 09:30
3 Lists.v, Poly.v 2014/10/01 09:30
4 MoreCoq.v, Logic.v 2014/10/08 09:30
5 Rel.v, Prop.v 2014/10/15 09:30
6 MoreMoreInd.v 2014/10/22 09:30
7 MoreLogic.v, Imp.v 2014/11/05 09:30
8 See here 2014/12/10 09:30
9 See here 2014/12/12 09:30


Install Coq

  • Download Coq here and install it.

    • For OS X, download those with CoqIDE bundle. And you may have to properly set path variable. add the following in ~/.bashrc: export PATH=/Applications/CoqIdE_8.4pl4.app/Resources/bin/:$PATH The path may be updated; be cautious before blindly adding the line.
  • Test by coqc -v in the command line.

Install Git

Download here.

Coq on Emacs

If you are interested in using Coq in Emacs, follow this instruction.

  • Install Emacs.

    • For OS X, download here.
  • Edit .emacs for Coq.

    • Here is a sample .emacs forCoq. Lines containing proof or coq are relavent.
  • Open .v files in Emacs, and interactively use Coq. Here are some useful commands; try them.

    • C-c C-n

    • C-c C-p

    • C-c C-Enter

    • C-c C-b

    • C-c C-x

    • C-c C-a C-c

    • C-c C-a C-p

    • C-c C-a C-a

    • Combination that begins with C-c