15-317 Constructive Logic

Fall 2012
Karl Crary
TuTh 12:00-1:20
NSH 3002
Recitation Sec A, Wed 12:30-1:20, PH A18B
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, 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, model-checkers

Course Information

Lectures TuTh 12:00-1:20, NSH 3002, Karl Crary
Recitations Section A, Wed 12:30-1: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 two-sided sheet of notes permitted.
Midterm II TBA, in class, 150 points.
One two-sided sheet of notes permitted.
Final TBA, 300 points.
Open notes.
Home http://www.andrew.cmu.edu/course/15-317/
Newsgroup academic.cs.15-317
Directory /afs/andrew.cmu.edu/scs/cs/15-317/

Teaching Staff

    Office Office Hours Phone Email
Lecturer Karl Crary GHC 9217 Tue 4:30-5:30 x8-7687 crary@cs
Teaching Assistant Carlo Angiuli GHC 6001 Wed 11:00-12:00 x8-1964 cangiuli@cs

[ Home | Schedule | Assignments | Software ]