
15399, 80317/617

Fall 2001 
Steve Awodey 
MW 3:304:50 
DH A317 
Recitation, Fri 3:304:50, DH A317 
9 units 
This multidisciplinary junior/seniorlevel 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:304:50, DH A317, Steve Awodey 

Recitations 
F 3:304:30, DH A317, Brigitte Pientka, Orlin Vakarelov 
Prerequisites 
CS Majors: 15151 or equivalent and
15212 Philosophy Majors: one programming course and either 80210 or 80211 Mathematics Majors: 21127 and one of 21228, 21484, 21373, 21132 
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. 
PreTest 
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 twosided sheet of notes permitted. 
Midterm II 
Wednesday, Nov 7, in class. Closed book, one twosided sheet of notes permitted. 
PostTest 
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/80317/ 
Newsgroup  academic.cs.15399
Email to bb+academic.cs.15399@andrew.cmu.edu. 
Directory  /afs/andrew.cmu.edu/course/80/317/ 
Office  Office Hours  Phone  

Lecturer  Steve Awodey  BH 152  Th 3:004:00  x88947  awodey@cmu.edu 
TA  Brigitte Pientka  WeH 8402  Tue 11:0012:00  x83076  bp@cs.cmu.edu 
TA  Orlin Vakarelov  BH 161A  M 1:002:00  x88573  okv@andrew.cmu.edu 
Exec. Asst.  Renee Shaeffer  BH 135  x88568  rs5s+@andrew.cmu.edu 
[ Home  Schedule  Assignments  Handouts  Software  Overview ]