| |
15-317 Constructive Logic
| Fall 2008 |
| Frank Pfenning |
| TuTh 12:00-1:20 |
| SH 222 |
| Recitation Sec A, Wed 11:30-12:20, SH 214 |
| 9 units |
This multidisciplinary junior/senior-level course is designed to provide a
thorough introduction to modern constructive logic, its roots in philosophy,
its numerous applications in computer science, and its mathematical
properties. Some of the topics to be covered are intuitionistic logic,
inductive definitions, functional programming, type theory,
connections between classical and constructive logic, logic programming,
decidable classes, temporal logic, model checking.
What's New?
Class Material
| Schedule |
Lecture schedule, readings, and code |
| Assignments |
Assignments, due dates, and policies |
| Handouts |
Course handouts |
| Software |
Proof checkers, language implementations, model-checkers |
Course Information
| Lectures |
TuTh 12:00-1:20, SH 222, Frank Pfenning |
| Recitations |
Section A, Wed 11:30-12:20, SH 214, Dan Licata
|
| Textbook |
There is no textbook.
Notes will be handed out throughout the class.
|
| Credit |
9 units |
| Grading |
40% Homework and Tests, 15% Midterm I, 15% Midterm II, 30% Final |
| Homework |
Weekly homework is assigned each Thursday and due the following Thursday.
3 late days can be used throughout the semester.
Homework assignments are worth a total of 400 points.
|
| Midterm I |
Thu Oct 2, in class, 150 points.
Closed book, one two-sided sheet of notes permitted.
|
| Midterm II |
Thu Nov 6, in class, 150 points.
Closed book, one two-sided sheet of notes permitted.
|
| Final |
Time and place TBA, 300 points.
Open book.
|
| Topics |
Intuitionistic Logic, Inductive Definitions,
Functional Programming, Type Theory,
Logic Programming,
Classical Logic, Decidable Classes,
Temporal Logic, Model Checking
|
| Home |
http://www.cs.cmu.edu/~fp/courses/15411-f08/ |
| Newsgroup |
academic.cs.15-317 |
| Directory |
/afs/andrew.cmu.edu/scs/cs/15-317/ |
Teaching Staff
| |
|
Office |
Office Hours |
Phone |
Email |
| Lecturer |
Frank Pfenning |
WeH 8117 |
W 2:00-3:00 |
x8-6343 |
fp@cs |
| Section A |
Dan Licata |
WeH 5130 |
M 2:00-3:00 |
x8-3052 |
drl@cs |
[ Home
| Schedule
| Assignments
| Handouts
| Software
]
fp@cs
Frank Pfenning
|