CSE-433 Logic in Computer Science
[ Home
| Schedule
| Assignments
| Software
| Resources
| Students
]
gla@postech Sungwoo Park
| Fall 2009 |
| 박성우, Sungwoo Park |
| Lecture, Tuesday and Thursday 11:00am - 12:15pm, 무은재 309호 |
| 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?
- (Oct 22) Midterm is out. It is due at 11am, Oct 25.
- (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, 무은재 309호 |
| Textbook |
Course notes [PS, PDF].
|
| Note |
Document on the disciplinary policy [PDF] |
| Credit |
3 |
| Grading (tentative) |
60% Assignments
20% Midterm Exam
20% Final Exam |
| Midterm |
72 hours Coq programming.
2007 Exam [PS, PDF]
Solution [PS, PDF]
2006 Exam [PS, PDF]
Solution [PS, PDF]
|
| Final |
TBA, 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 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 |
Engineering Building 2, Room 309 |
| Office Hour |
Tuesday 5pm-6pm |
| Teaching assistant |
임현승, Hyeonseung Im, genilhs@postech
|
[ Home
| Schedule
| Assignments
| Software
| Resources
| Students
]
gla@postech Sungwoo Park
|