CSE-433 Logic in Computer Science

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

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.

Class Material

Course Information

Teaching Staff