CSE-433 Logic in Computer Science

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


Fall 2007
박성우, Sungwoo Park
Lecture, Tuesday and Thursday 11:00am - 12:15pm, 정통연 143호
3 credits

This course covers the basics of logic in computer science. We will 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.
Topics to be covered include: propositional logic, natural deduction, normalization, Curry-Howard isomorphism, sequent calculus, cut-elimination, classical logic, first-order logic, and dependent types.

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


What's New?

  • (Dec 18) The course is over.
  • (Dec 4) Makeup lecture: in the classroom, 7:00pm, Dec 12.
  • (Oct 28) Midterm solution is up.
  • (Sep 27) Makeup lecture: in the classroom, 11:45am, Sep 28 - Lunch to be served!
  • (Sep 6) Makeup lecture: in the classroom, Sep 7.
  • (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, 정통연 143호
Textbook Course notes [PS, PDF] will be distributed.
Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Yves Bertot and Perre Casteran. Springer. (Supplementary)
Note Document on the disciplinary policy [PDF]
Credit 3
Grading 50% Quizzes and Assignments
25% Midterm Exam
25% Final Exam
Midterm Oct 25 (Thursday), 10am - 1pm, classroom. Closed book.
2006 Exam [PS, PDF] Solution [PS, PDF]
Final Dec 18 (Tuesday), 7pm - 10pm (3 hours). Closed book. Engineering building 109 (공학2동 109호)
2006 Exam [PS, PDF] Solution [PS, PDF]
Home http://www.postech.ac.kr/~gla/cs433/
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 assistants 김태경, Taekyung Kim, strikerz@postech
김진하, Jinha Kim, goldbar@postech

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