shuuki4/pl2016

Programming Languages, SNU 4190.310, 2016 Spring

• Instructor: Prof. Chung-Kil Hur
• TA: Jeehoon Kang
  • Email address: pl2016@sf.snu.ac.kr.
    • Send emails for personal matters only. Use the GitHub repository issue tracker.
    • DO NOT send emails to jee...@sf.snu.ac.kr.
    • In the case you send TA an email, specify your name and your student ID.
  • Place: Bldg 301 Rm 554-1
  • Office Hour: Please email me to make an appointment.

Announcements

• There will be a lab session on 2016/03/08 (Tue).

Assignments

Due	Description	Notes
NO	Assignment 00	No scores

Must Read

• READ VERY CAREFULLY this section.

Grading

• Assignments: 45%
  • Coq problems in the software foundations material. Read carefully the next subsections.
• 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.

Questions

• In class: if you speak Korean, ask in Korean. Otherwise, ask in English.
• In the GitHub repository issue tracker: ask in English.
• Send email for PERSONAL MATTERS ONLY.
• If you want to post a piece of source code, please DO NOT upload an image of it. Because it is hard to reconstruct texts from images.
  • Instead, use GitHub Markdown's "fenced code blocks" feature.
  • Or, you can always use GitHub Gist.

Coq

• 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
    • Install Coq for Windows
    • Install Coq for OS X

• Use IDEs supporting Coq.

  • CoqIDE: Download those bundled with CoqIDE in the Download page.
    • In OS X, at first run, you may see an error message saying "Failed to load coqtop." Then click "No", and then find /Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/coqtop and open for once. Then goto CoqIDE > Preferences > Externals. And then change coqtop into /Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/coqtop.
  • Emacs: Company-Coq. Follow the setup instructions.

Textbook: Software Foundations

• The textbook is in this repository's sf/ directory.
• DO NOT DOWNLOAD the textbook from The official Software Foundation website in order to keep in sync.

Assignment

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..

Submission

• 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.
• Edit P??.v files to do the assignment.
• make to compile your submission. make eval to grade your submission yourself.
• Both make and make eval SHOULD SUCCEED. If not, your score will be 0.
• Check your submission by ../check.sh
  • P??.v files SHOULD NOT contain admit and Admitted.
  • If a P??.v file contains string GIVEUP, then it will be scored 0.
• Submit at: http://147.46.15.109:9480/
  • DO NOT ATTACK. Please.
  • DO NOT USE A STRONG PASSWORD. It is http.
  • If your submission status is SYSTEM ERROR or RUNNING for a long time, please ask the TA.

Misc.

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