CSE-433 Logic in Computer Science

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


Fall 2009
박성우, Sungwoo Park
Lecture, Tuesday and Thursday 11:00am - 12:15pm, 무은재 309호
3 credits

This course covers the basics of logic in computer science. We study various styles of formulating logic, but the main focus of this course lies on a proof-theoretic study of constructive logic, as opposed to a model-theoretic study of classical logic. A proof-theoretic formalization of constructive logic serves as a foundation for type theory for programming languages, so this course should also be interesting to those interested in type theory. We also learn to program in a proof assistant Coq which enables us to formally write proofs in a logical language.
Topics to be covered include: propositional logic, natural deduction, normalization, Curry-Howard isomorphism, first-order logic, dependent types, sequent calculus, cut-elimination, classical logic, modal logic, substructural logic, and automatic theorem proving.

Prerequisites: CSE-321 Programming Languages, or by permission of the instructor.


What's New?

  • (Oct 22) Midterm is out. It is due at 11am, Oct 25.
  • (Sep 1) Welcome -- Course webpage is open!

Class Material

Schedule Lecture schedule and readings
Assignments Details of assignments, due dates, and policies
Software Guides to setting up the programming environment
Resources Course resources

Course Information

Lectures Tuesday and Thursday 11:00am - 12:15pm, 무은재 309호
Textbook Course notes [PS, PDF].
Note Document on the disciplinary policy [PDF]
Credit 3
Grading (tentative) 60% Assignments
20% Midterm Exam
20% Final Exam
Midterm 72 hours Coq programming.
2007 Exam [PS, PDF] Solution [PS, PDF]
2006 Exam [PS, PDF] Solution [PS, PDF]
Final TBA, Take-home.
2007 Exam [PS, PDF] Solution [PS, PDF]
2006 Exam [PS, PDF] Solution [PS, PDF]
Home http://www.postech.ac.kr/~gla/cs433/
Fall 2007 http://pl.postech.ac.kr/~gla/lics2007/
Fall 2006 http://pl.postech.ac.kr/~gla/lics2006/
Discussion telnet to pl.postech.ac.kr with id bbs
Directories /afs/postech.ac.kr/class/cse/cs433/handin/ for submission of assignments

Teaching Staff

Instructor 박성우, Sungwoo Park
Contact gla@postech or x-2386
Office Engineering Building 2, Room 309
Office Hour Tuesday 5pm-6pm
Teaching assistant 임현승, Hyeonseung Im, genilhs@postech

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