
15317 Constructive Logic
Fall 2013 
Penny Anderson 
TuTh 12:001:20 
NSH 3002 
Recitation Sec A, Wed 12:301:20, WeH 6423 
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,
linear logic.
Class Material
Schedule 
Lecture schedule, readings, and code 
Assignments 
Assignments, due dates, and policies 
Handouts 
Course handouts 
Software 
Proof checkers, language implementations, modelcheckers 
Course Information
Textbook 
There is no textbook.
Notes will be handed out throughout the class.

Grading 
40% Homework, 15% Midterm I, 15% Midterm II, 30% Final 
Homework 
Most weeks 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 20% from an
assignment's total possible score.)
Homework assignments are worth a total of 400 points.

Midterm I 
Thu Oct 3, in class, 150 points.
Closed book, one twosided sheet of notes permitted.

Midterm II 
Thu Nov 7, in class, 150 points.
Closed book, one twosided sheet of notes permitted.

Final 
Time and place TBD, 300 points

Topics 
Intuitionistic Logic, Natural Deduction, Sequent Calculus, Inductive Definitions,
Functional Programming, Type Theory,
Logic Programming,
Classical Logic, Linear Logic

Piazza discussion group 

Teaching Staff


Office 
Office Hours 
Phone 
Email 
Lecturer 
Penny Anderson 
GHC 6025 
Tue, Thu 2:00  3:00 and by appointment 
x83413
 annpenny at Andrew 
Teaching Assistant 
Michael Sullivan 
GHC 9005 
Wed, Fri 3:00  4:00 
x85940 
mjsulliv at Andrew 
[ Home
 Schedule
 Assignments
 Handouts
 Software
]
annpenny at Andrew
