
15317 Constructive Logic
Fall 2012 
Karl Crary 
TuTh 12:001:20 
NSH 3002 
Recitation Sec A, Wed 12:301:20, PH A18B 
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, logic programming,
proof search, logical frameworks.
See Constructive
Logic, Fall 2009 for information on a prior version of this course.
What's New?
Class Material
Schedule 
Lecture schedule, readings, and code 
Assignments 
Assignments, due dates, and policies 
Software 
Proof checkers, language implementations, modelcheckers 
Course Information
Lectures 
TuTh 12:001:20, NSH 3002, Karl Crary 
Recitations 
Section A, Wed 12:301:20, PH A18B, Carlo Angiuli

Textbook 
There is no textbook.

Credit 
9 units 
Grading 
40% Homework, 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.
(Each late day beyond the 3 free ones will deduct 25% from an
assignment's total possible score.)
Homework assignments are worth a total of 400 points.

Midterm I 
TBA, in class, 150 points.
One twosided sheet of notes permitted.

Midterm II 
TBA, in class, 150 points.
One twosided sheet of notes permitted.

Final 
TBA, 300 points.
Open notes.

Home 
http://www.andrew.cmu.edu/course/15317/ 
Newsgroup 
academic.cs.15317 
Directory 
/afs/andrew.cmu.edu/scs/cs/15317/ 
Teaching Staff


Office 
Office Hours 
Phone 
Email 
Lecturer 
Karl Crary 
GHC 9217 
Tue 4:305:30 
x87687 
crary@cs 
Teaching Assistant 
Carlo Angiuli 
GHC 6001 
Wed 11:0012:00 
x81964 
cangiuli@cs 
[ Home
 Schedule
 Assignments
 Software
]
