CSE-433 Logic in Computer Science - Assignments

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park

Words on academic integrity

  • Be sure to read the document on the disciplinary policy for this course. [PDF]
  • Even when you are allowed to discuss assignments with other students, what you hand in must be entirely your own work. This means that when it comes to writing your code or written solution, it must be entirely your own work. That is, you have to write code and written solution all on your own. Hence you should never look at your classmates' code or written solution, not to mention showing yours to them, even if you have discussed assignments with them.
  • If you use outside material, you must provide all proper citations:
    • "I used the following outside material to complete this assignment: (sources of outside material)."
  • If we judge that you have copied any part of other students' code or written solution, you will be punished for cheating.
  • Cheating also includes plagiarism in the sense of stealing someone else's idea.
  • You should never post code relevant to assignments on the discussion board.

프로그래밍 숙제는 모두 handin/hw1/HemosID/ 에 복사해 주세요!

   Out    Points    Assignment    Due    Solution

W1    9.3 0 Inductive proofs [PDF]   By class, Sep 10
P1    9.5 100 Propositional logic [coq1.v]   11:59pm, Sep 12 allhw1.zip
W2    9.10 100 Proof trees [PDF]   By class, Sep 17
P2    9.12 100 Inductive set [coq2.v] [coq2.pdf]   11:59pm, Sep 26 (2 weeks) allhw2.zip
P3    9.12 100 Proof terms [coq3-1.v] [coq3-1.pdf]   11:59pm, Sep 19 allhw3-1.zip
P4    9.17 100 First order logic [coq3-2.v] [coq3-2.pdf]   11:59pm, Oct 1 (2 weeks) allhw3-2.zip
P5    10.3 200 Inductive datatypes
[coq4.v] [coq4-2.v] [coq4.pdf]
  11:59pm, Oct 17 (2 weeks) allhw4.zip
P6    10.10 100 Inductive datatypes [coq4-3.v]   11:59pm, Oct 17 allhw4-3.zip
P7    10.17 100 Inductive predicates [coq5.v] [coq5.pdf]
Inductive proofs [coq6.v] [coq6.pdf]
  11:59pm, Oct 24 allhw5.zip
W3    10.22 100 Normalization [PDF]   By class, Oct 29
P8    10.24 100 Pythagorean theorem [coq7.v] [coq7.pdf]   11:59pm, Oct 31 allhw7.zip
W4    10.31 100 Cut elimination [PDF]   By class, Nov 7
Midterm    10.31 100 Verification of an interpreter [PDF] [midterm13.v]   (72 hours) 11:59pm, Nov 3
P9    11.7 100 Type safety of the simply-typed lambda calculus
[coq8.v, LibTactics.v, LibNat.v] [coq8.pdf]
  11:59pm, Nov 21 (2 weeks)
P10    11.28 100 Decision procedure [PDF] [prover.zip] [proptest.sml]   11:59pm, Dec 12 (2 weeks)

P = Programming, W = Written, (points) = Extra-credit

  • No late submissions will be accepted.
  • Your hand-in directory is /afs/postech.ac.kr/class/cse/cs433/handin/.

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park