CSE-433 Logic in Computer Science

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

Fall 2014
박성우, Sungwoo Park
Lecture, Tuesday and Thursday 12:30pm - 1:45pm, 수리과학관 206호
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 automated theorem proving.

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

What's New?

  • (Dec 9) Final: Dec 15 Monday 7pm-10pm, Engineering building 2동 111, closed book.
  • (Nov 6) Midterm is out! See Assignments.
  • (Sep 2) 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 2:00pm - 3:15pm, 수리과학관 206호
Textbook Course notes [PS, PDF].
Note Document on the disciplinary policy [PDF]
Credit 3
Grading 60% Assignments
20% Midterm Exam
20% Final Exam
Midterm 2011 Exam: 72 hours Coq programming + Written [PDF].
2010 Exam: 72 hours Coq programming.
2009 Exam: 72 hours Coq programming.
2007 Exam [PS, PDF] Solution [PS, PDF]
2006 Exam [PS, PDF] Solution [PS, PDF]
Final 2013 Exam [PDF]
2011 Exam [PDF]
2010 Exam [PDF] Solution [PDF]
2009: Take-home.
2007 Exam [PS, PDF] Solution [PS, PDF]
2006 Exam [PS, PDF] Solution [PS, PDF]
Home http://pl.postech.ac.kr/~gla/cs433/
Fall 2013 http://pl.postech.ac.kr/~gla/lics2013/
Fall 2011 http://pl.postech.ac.kr/~gla/lics2011/
Fall 2010 http://pl.postech.ac.kr/~gla/lics2010/
Fall 2009 http://pl.postech.ac.kr/~gla/lics2009/
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

Teaching Staff

Instructor 박성우, Sungwoo Park
Contact gla@postech or x-2386
Office 정통연, Room 334
Office Hour Thursday 3:30pm-4:30pm
Teaching assistant TBA

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