|
15-399, 80-317/617
|
| Fall 2001 |
| Steve Awodey |
| MW 3:30-4:50 |
| DH A317 |
| Recitation, Fri 3:30-4:50, DH A317 |
| 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, decidable classes, temporal logic, model checking.
| Schedule | |
|---|---|
| Assignments | |
| Handouts | |
| Software | |
| Overview |
| Lectures | MW 3:30-4:50, DH A317, Steve Awodey |
|---|---|
| Recitations |
F 3:30-4:30, DH A317, Brigitte Pientka, Orlin Vakarelov |
| Prerequisites |
CS Majors: 15-151 or equivalent and
15-212 Philosophy Majors: one programming course and either 80-210 or 80-211 Mathematics Majors: 21-127 and one of 21-228, 21-484, 21-373, 21-132 |
| Textbook |
Logic in Computer Science, Huth and Ryan, CUP 2000. Lecture 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 Monday and due the following Monday. Late homework will be accepted only under exceptional circumstances. |
| Pre-Test |
Wednesday, Aug 31, in recitation. You are required to take this test. Every answer receives full credit. |
| Midterm I |
Wednesday, Oct 10, in class. Closed book, one two-sided sheet of notes permitted. |
| Midterm II |
Wednesday, Nov 7, in class. Closed book, one two-sided sheet of notes permitted. |
| Post-Test |
Monday, Dec 10, in class. You are required to take this test. Every answer receives full credit. |
| Final |
To be scheduled Open book. |
| Topics |
Intuitionistic Logic, Inductive Definitions, Functional Programming, Type Theory, Classical vs. Constructive Logic, Decidable Classes Temporal Logic, Model Checking |
| Home | http://www.andrew.cmu.edu/course/80-317/ |
| Newsgroup | academic.cs.15-399
Email to bb+academic.cs.15-399@andrew.cmu.edu. |
| Directory | /afs/andrew.cmu.edu/course/80/317/ |
| Office | Office Hours | Phone | |||
|---|---|---|---|---|---|
| Lecturer | Steve Awodey | BH 152 | Th 3:00-4:00 | x8-8947 | awodey@cmu.edu |
| TA | Brigitte Pientka | WeH 8402 | Tue 11:00-12:00 | x8-3076 | bp@cs.cmu.edu |
| TA | Orlin Vakarelov | BH 161A | M 1:00-2:00 | x8-8573 | okv@andrew.cmu.edu |
| Exec. Asst. | Renee Shaeffer | BH 135 | x8-8568 | rs5s+@andrew.cmu.edu |
[ Home | Schedule | Assignments | Handouts | Software | Overview ]