No description, website, or topics provided.
HTML Coq OCaml Verilog Makefile CSS
Switch branches/tags
Nothing to show
Clone or download

Programming Languages, SNU 4190.310, 2016 Spring

  • Instructor: Prof. Chung-Kil Hur
  • TA: Jeehoon Kang
    • Email address:
      • Send emails for administrative matters only. Use the GitHub repository issue tracker.
      • DO NOT send emails to
      • In the case of sending TA an email, specify sender's name and student ID.
    • Place: Bldg 301 Rm 554-1
    • Office Hour: Thursday 18:15-19:00. In the case of needing an extra time, please email me to make an appointment.



Due Due (Delay) Description Points
20160612 23:59 20160617 23:59 Assignment 13 60
20160605 23:59 20160612 23:59 Assignment 12 100
20160529 23:59 20160605 23:59 Assignment 11 160
20160522 23:59 20160529 23:59 Assignment 10 120
20160517 23:59 20160522 23:59 Assignment 09 60
20160508 23:59 20160517 23:59 Assignment 08 130
20160503 23:59 20160508 23:59 Assignment 07 120
20160424 23:59 20160503 23:59 Assignment 06 300
20160417 23:59 20160424 23:59 Assignment 05 130
20160410 23:59 20160417 23:59 Assignment 04 260
20160403 23:59 20160410 23:59 Assignment 03 130
20160327 23:59 20160403 23:59 Assignment 02 100
20160320 23:59 20160610 23:59 Assignment 01 70
NO NO Assignment 00 No scores

Must Read

  • READ VERY CAREFULLY this section.


  • Assignments: 45%
  • Exams: 50% (mid-term 20% and final 30%)
    • You will solve Coq problems at the lab during the exam.
  • Attendance: 5%
    • -1% per absence. IMPORTANT: 6 absences make an F.



  • Use Coq 8.4pl5. DO NOT use Coq 8.5!

    • If not, your submissions (assignments & exams) will not be properly graded.
  • Install Coq.

    • Linux
      • Install opam, and make sure you can use OCaml 4.02.3.
      • Install libgtk2 by sudo apt-get install libgtk2.0-dev or sudo yum install gtk2-devel.
      • Install lablgtk2 by opam install lablgtk
      • Download tarball file.
      • Extract the tarball, ./configure -coqide opt, make, and then make install.
      • Test by coqc -v in the command line. Check your PATH variable if you get an error.
      • Run CoqIDE by coqide.
    • For Windows / OS X
  • Use IDEs supporting Coq.

  • Install Cygwin in Windows.

    • If you use Unix-like OS, just ignore it.
    • Download Cygwin. CAUTION: choose 32- or 64-bit versions correctly.
    • Install Cygwin. Make sure that you install bash and make (in Select packages). Installation may take a long time.
    • Now by "terminal" I mean the Cygwin terminal.
  • Add the directory that contains Coq binaries in the PATH variable.

    • Edit your Shell init file (like ~/.bashrc or ~/.bash_profile).
      • For Cygwin, find the file in C:\cygwin\home\[USER_ID].
    • Add export PATH=$PATH:[THE_DIRECTORY_CONTAINS_COQ] at the end of the file.
    • Check which coqc in the terminal. It should point to the coqc binary.
      • Restart the terminal to apply ~/.bashrc.
    • For Windows, the directory is highly likely /cygdrive/c/Program\ Files\ \(x86\)/Coq/bin/.
      • NOTE: DO NOT USE C:\Program Files (x86)\Coq\bin. In Cygwin, C: is recognized as /cygdrive/c.
    • For OS X, the directory is highly likely /Applications/
    • For Linux, PATH may already contain the directory. Check by which coqc.

Textbook: Software Foundations


  • Assignments will be issued every Thursday. The deadline is the next Sunday (10 days later). The deadline for the delayed submission is the next to the next Sunday (17 days later).
    • Exception: The delayed submission for the Assignment 01 will be accepted until the end of the semester.

Honor Code: DO NOT CHEAT

  • If you copy others' source code, you will get F.
  • "Others' source code" includes other students' and resources around the web. Especially, do not consult with public repositories on software foundations.
  • Note that we have a good automatic clone detector. I found out that a lot of students cheated last time. I hope we all be happy at the end of the semester..
  • The maximum score of a delayed submission is 80% that of a regular submission.
    • The granularity the delayed submission is per-problem, not per-assignment. So even if you couldn't get the full score for the regular submission period, try to solve the remaining problems and submit them.


  • assignments/$NAME directory is the assignment $NAME.
    • You submit P??.v files. You should edit only P??.v. DO NOT TOUCH ANYTHING ELSE.
    • E??.v files are for evaluation.
    • Everything else are for relevant the definitions for the assignment.
  • make in the terminal to compile files so that IDE can understand them.
  • Edit P??.v files to do the assignment.
  • make in the terminal to compile your submission. make eval in the terminal to grade your submission yourself.
  • Both make and make eval SHOULD SUCCEED. If not, your score will be 0.
  • make eval will check your submission.
    • P??.v files SHOULD NOT contain admit, Admitted, and anything in forbidden.txt.
    • If a P??.v file contains string GIVEUP, then it will be scored 0.
  • make submission to prepare your submission.
    • zip should be installed. Otherwise, you can just zip P??.v.
  • Submit at:
    • DO NOT ATTACK. Please.
    • If your submission status is SYSTEM ERROR or RUNNING for a long time, even after refreshing your web browser for several times, please ask the TA.


  • If something bad happens, please download the most recent version of the assignments.

  • You may have to make before interacting with IDEs.

  • You can specify the CRLF handling strategy in Git (cf). In Windows, some strategies may break the Makefile. Please just use the linebreaks as in the repository.

  • When running CoqIDE in OS X for the first time, you may see an error message saying Failed to load coqtop. Then click No, and then find /Applications/ and open for once. Then goto CoqIDE > Preferences > Externals. And then change coqtop into /Applications/

  • Your submission file should have alphanumeric characters only (#30).

  • If cygwin complains like ./ line 2: $'\r': command not found, please:

    • Install dos2unix in Cygwin.
    • Run: dos2unix
  • If you use Coquille (on Vim) and your terminal is hidden by some message (warning (some rule has been masked)), please edit ~/.vim/.../coquille/autoload/'s restart_coq as follows (NOTE: stderr = subprocess.PIPE):

      def restart_coq(*args):
      global coqtop
      if coqtop: kill_coqtop()
          coqtop = subprocess.Popen(
                  ["coqtop", "-ideslave"] + list(args),
                  stdin = subprocess.PIPE,
                  stdout = subprocess.PIPE,
                  stderr = subprocess.PIPE,
                  preexec_fn = ignore_sigint
      except OSError:
          print("Error: couldn't launch coqtop")

    Thank you for reporting, @indiofish


  • I strongly recommend you to use Git for the course. Register at GitHub. Try Git.