CSE-490 Logic in Computer Science - Schedule

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


  • Lectures are Monday and Wednesday 13:15pm - 14:30pm, 무은재기념관 307호.
  • 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    Assignment Due

Mon Sep 4   Judgments, Inductive proofs, Derivable rules, Admissible rules CSE-321 Programming Languages Course Notes Chapter 2 [PS, PDF]
Wed Sep 6   Propositions, Propositional logic (conjunction, implication, truth), 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]

Mon Sep 11   Propositional logic (disjunction, falsehood), Notational definition, Logical equivalence
Wed Sep 13   Hypothetical judgments, Substitution principle, Structural properties Assignment 1

Mon Sep 18   Local soundness and completeness
Wed Sep 20   Proof reduction and expansion

Mon Sep 25   Normal proofs Assignment 2
Wed Sep 27   Normalization

Mon Oct 2   Curry-Howard isomorphism CS Chapter 2 [PS, PDF]
Wed Oct 4   Properties of proof terms

Mon Oct 9   Sequent calculus CS Chapter 3 [PS, PDF]
Wed Oct 11   Cut elimination

Mon Oct 16   Proof of normalization Assignment 3
Wed Oct 18   First-order logic (1) CS Chapter 4 [PS, PDF]

Midterm, Wednesday, Oct 25, 1:15pm -- 2:45pm, in the classroom. Closed book.
Exam [PS, PDF] Solution [PS, PDF]

Mon Oct 30   First-order logic (2)
Wed Nov 1   First-order logic (3)

Mon Nov 6   Inductive datatypes, primitive recursion CS Chapter 5 [PS, PDF]
Wed Nov 8   (no class)

Mon Nov 13   Predicate on terms
Wed Nov 15   Induction

Mon Nov 20   First-order logic with datatypes
Wed Nov 22   Classical logic, sequent calculus for classical logic CS Chapter 6 [PS, PDF]

Mon Nov 27   Double negation translation, CPS transformation
Wed Nov 29   Linear logic Lecture notes by Frank Pfenning (PDF).
Chapters 1 and 2.

Mon Dec 4   Dual intuitionistic linear logic
Wed Dec 6   Linear lambda-calculus Section 6.1 of Pfenning

Mon Dec 11   (no class)
Wed Dec 13   Modal logic Slide by Hyeonseung Im
Paper: A judgmental reconstruction of modal logic. Pfenning and Davies. [PDF] [PS]
Fri Dec 15   Introduction to Coq
Mueunjae 309, 1:15pm
[PPT]

Final Exam Dec 20, 1pm - 4pm (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