CSE433 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
[coq31.v]
[coq31.pdf]
 
11:59pm, Sep 19 
allhw31.zip

P4 
9.17 
100 
First order logic
[coq32.v]
[coq32.pdf]
 
11:59pm, Oct 1 (2 weeks) 
allhw32.zip

P5 
10.3 
200 
Inductive datatypes
[coq4.v]
[coq42.v]
[coq4.pdf]
 
11:59pm, Oct 17 (2 weeks) 
allhw4.zip
allhw42.zip

P6 
10.10 
100 
Inductive datatypes
[coq43.v]
 
11:59pm, Oct 17 
allhw43.zip

P7 
10.17 
100 
Inductive predicates
[coq5.v]
[coq5.pdf]
Inductive proofs
[coq6.v]
[coq6.pdf]
 
11:59pm, Oct 24 
allhw5.zip
allhw6.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 simplytyped 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) = Extracredit
 No late submissions will be accepted.
 Your handin directory is /afs/postech.ac.kr/class/cse/cs433/handin/.
[ Home
 Schedule
 Assignments
 Software
 Resources
 Students
]
gla@postech Sungwoo Park
