15-399 Constructive Logic

Fall 2000

Frank Pfenning

TuTh 10:30-11:50

BH A51

Recitation Sec A, Wed 10:30-11:20, DH A317, Steven Awodey

Recitation Sec B, Wed 11:30-12:20, DH A317, Andreas Abel

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, realizability, connections between classical and constructive logic, decidable classes, temporal logic, model checking.

What's New?

(Dec 22) The final has been gradesd and course grades assigned. A model solution is available, and you may view your final in the instructors office (WeH 8117)

Class Material

Schedule
Assignments
Handouts
Software
Overview

Course Information

Lectures	TuTh 10:30-11:15, BH A51, Frank Pfenning
Recitations	Section A, Wed 10:30-11:20, DH A317, Steven Awodey Section B, Wed 11:30-12:20, DH A317, Andreas Abel
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	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. Late homework will be accepted only under exceptional circumstances.
Pre-Test	Wednesday, Aug 20, in recitation. You are required to take this test. Every answer receives full credit.
Midterm I	Thursday, Oct 5, in class. Closed book, one two-sided sheet of notes permitted. Exam, Model Solution
Midterm II	Thursday, Nov 9, in class. Closed book, one two-sided sheet of notes permitted. Exam, Model Solution
Post-Test	Tuesday, Dec 12, in class. You are required to take this test. Every answer receives full credit.
Final	Tuesday, Dec 19, 5:30-8:30, BH A51 Open book. Final, Model Solution
Topics	Intuitionistic Logic, Inductive Definitions, Functional Programming, Type Theory, Realizability, Classical Logic, Decidable Classes Temporal Logic, Model Checking
Home	http://www.cs.cmu.edu/~fp/courses/logic/
Newsgroup	academic.cs.15-399 Email to bb+academic.cs.15-399@andrew.cmu.edu.
Directory	/afs/andrew.cmu.edu/scs/cs/15-399/

Teaching Staff

		Office	Office Hours	Phone	Email
Lecturer	Frank Pfenning	WeH 8117	W 2:30-3:30	x8-6343	fp@cs
Section A	Steven Awodey	BH 152	M 1:00-2:00	x8-8947	awodey@cmu.edu
Section B	Andreas Abel	WeH 8104	T 1:00-2:00	x8-2582	abel@cs.cmu.edu
Exec. Asst.	Maury Burgwin	WeH 8124		x8-4740	mburgwin@cs.cmu.edu

fp@cs
Frank Pfenning