CSE433 Logic in Computer Science
[ Home
 Schedule
 Assignments
 Software
 Resources
 Students
]
gla@postech Sungwoo Park
Fall 2010 
¹Ú¼º¿ì, 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 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 automatic theorem proving.
Prerequisites:
CSE321 Programming Languages,
or by permission of the instructor.
What's New?
 (Nov 11) Midterm is out  Check out your emails.
 (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 9:30am  10:45pm, Á¤Åë¿¬ 143È£ 
Textbook 
Course notes [PS, PDF].

Note 
Document on the disciplinary policy [PDF] 
Credit 
3 
Grading 
50% Assignments
20% Midterm Exam
30% Final Exam 
Midterm 
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 
2010 Exam [PDF]
Solution [PDF]
2009: Takehome.
2007 Exam [PS, PDF]
Solution [PS, PDF]
2006 Exam [PS, PDF]
Solution [PS, PDF]

Home 
http://www.postech.ac.kr/~gla/cs433/
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 x2386 
Office 
Á¤Åë¿¬, Room 334 
Office Hour 
Thursday 11am12pm 
Teaching assistant 
ÀÓÁ¤Ç¥, jplim@postech

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