CSE-433 Logic in Computer Science - Schedule

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


  • The schedule is subject to change throughout the semester.
  • CS = Course Notes. (The up-to-date version including all chapters [PS, PDF])

)
Date    Lecture   Reading    Quiz and Assignment Due

Tue Sep 4   Judgments, Inference rules, Inductive proofs
(No class - Inauguration ceremony. To be rescheduled: 10am, Sep 7, in the classroom)
CSE-321 Programming Languages Course Notes Chapter 2 [PS, PDF]
Thu Sep 6   Inductive proofs, Overview of logic

Thu Sep 11   Propositions, Propositional logic, Natural deduction CS Chapter 1 [PS, PDF]
On the Meaning of the Logical Constants and the Justification of the Logical Laws, Martin-Löf [HTML]
Truth of a Proposition, Evidence of a Judgement, Validity of a Proof, Martin-Löf [PDF]
Quiz 1
[PS, PDF ]
Thu Sep 13   Notational definition, Logical equivalence class-1.v Assignment 1

Tue Sep 18   Hypothetical judgments, Substitution principle, Structural properties
Thu Sep 20   Local soundness and completeness, Proof reduction and expansion Assignment 2

Tue Sep 25   (No class - Chusok)
Thu Sep 27   Normal proofs, Normalization

Tue Oct 2   Curry-Howard isomorphism
(Instructor out of town. To be rescheduled: 11:45am, Sep 28, in the classroom)
CS Chapter 2 [PS, PDF]
Thu Oct 4   Properties of proof terms
Assignment 3

Tue Oct 9   First-order logic - Introduction CS Chapter 3 [PS, PDF] Quiz 2
[PS, PDF ]
Thu Oct 11   First-order logic - Quantifications

Tue Oct 16   First-order logic - Soundness and completeness Assignment 4
Thu Oct 18   First-order logic - Proof terms

Midterm, Oct 25 (Thursday), 10am - 1pm, classroom. Closed book.
Exam [PS, PDF] Solution [PS, PDF]
Assignment 5
(Oct 23)

Tue Oct 30   Introduction to datatypes CS Chapter 5 [PS, PDF]
Thu Nov 1   Primitive recursion

Tue Nov 6   Predicate on terms
Thu Nov 8   Induction on terms

Tue Nov 13   Proof terms
Thu Nov 15   Examples of induction

Tue Nov 20   Induction on predicates Assignment 6
Thu Nov 22   Examples of induction on predicates

Tue Nov 27   Definitional equality Assignment 7
Thu Nov 29   Classical logic (Instructor out of town. To be rescheduled: 7:00pm, Dec 12, in the classroom) CS Chapter 6 [PS, PDF]

Tue Dec 4   CPS transformation Assignment 8
Thu Dec 6   Linear logic (I) Chapters 1 and 2 of Course Notes by Frank Pfenning

Tue Dec 11   Linear logic (II)
Thu Dec 13   Review

Final Exam Dec 18 (Tuesday), 7pm - 10pm (3 hours). Closed book. Engineering building 109 (2 109ȣ)
Exam [PS, PDF] Solution [PS, PDF]

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