CSE-433 Logic in Computer Science

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


Fall 2011
박성우, Sungwoo Park
Lecture, Tuesday and Thursday 9:30am - 10:45pm, 정통연 143호
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?

  • (Sep 1) Written assignment 1 is out.
  • (Sep 1) 3-hour makeup lecture: Sep 6, 7pm-10pm.
  • (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 9:30am - 10:45pm, 정통연 143호
Textbook Course notes [PS, PDF].
Note Document on the disciplinary policy [PDF]
Credit 3
Grading 60% Assignments
20% Midterm Exam
20% Final Exam
(tentative)
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 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://www.postech.ac.kr/~gla/cs433/
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
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 정통연, Room 334
Office Hour Thursday 11am-12pm
Teaching assistant 서정봉, baramseo@postech

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