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 to the discussion board.
   Out    Points    Assignment    Due      Solution
W1    Thu Sep 1   0 Inductive proofs [PDF]   By class, Sep 6
P1    Tue Sep 6   100 Propositional logic [coq1.v]   11:59pm, Sep 15
W2    Thu Sep 15   100 Proof trees[PDF]   By class, Sep 22
P2    Thu Sep 15   100 Inductive set [coq2.v] [coq2.pdf]   11:59pm, Sep 22
W3    Thu Sep 22   100 Substitution[PDF]   By class, Sep 29
P3    Thr Sep 22   100 Proof terms and first order logic [coq3.v] [coq3.pdf]   11:59pm, Sep 29
P4    Thr Oct 6   200 Inductive datatypes
[coq4.v] [coq4-2.v] [coq4-3.v] [coq4.pdf] 		  11:59pm, Oct 13 [coq4-sol.v] [coq4-2-sol.v] [coq4-3-sol.v]
P5    Tue Oct 13   200 Inductive predicates [coq5.v] [coq5.pdf]
Inductive proofs [coq6.v] [coq6.pdf] 		  11:59pm, Oct 27 [coq5sol.v] [coq6sol.v]
P6    Tue Nov 3   100 Pythagorean theorem [coq7.v] [coq7.pdf]   11:59pm, Nov 10 [coq7sol.v]
P7    Thr Nov 10   100 Type safety of simply-typed lambda calculus [coq8.v, LibTactics.v, LibNat.v] [coq8.pdf]   11:59pm, Nov 22
P8    Thr Nov 22   100 Certifying programs [coq9.v]   11:59pm, Nov 29
P9    Thu Nov 29   100 Decision procedure [PDF] [prover.zip]   By class, Dec 13
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