CSE433 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 prooftheoretic study of
constructive logic, as opposed to a modeltheoretic study of classical logic.
A prooftheoretic 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, CurryHoward isomorphism,
firstorder logic, dependent types, sequent calculus, cutelimination, classical logic, modal logic,
substructural logic, and automated theorem proving.
Prerequisites:
CSE321 Programming Languages,
or by permission of the instructor.
What's New?
 (Dec 9) Final: Dec 15 Monday 7pm10pm, 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: Takehome.
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 x2386 
Office 
Á¤Åë¿¬, Room 334 
Office Hour 
Thursday 3:30pm4:30pm 
[ Home
 Schedule
 Assignments
 Software
 Resources
 Students
]
gla@postech Sungwoo Park
