15-317 Constructive Logic

Fall 2010

Karl Crary

TuTh 12:00-1:20

GHC 4102

Recitation Sec A, Wed 12:30-1:20, WeH 4623

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?

(12/3) Solutions to Assignments 8 and 9 are now available.
(11/24) Twelf code from November 19 and 23 is now available.
(11/24) Twelf code and notes on adequacy from November 11 are now available.
(10/22) The Theorem Prover in Elf written during lecture is now available.
(10/22) The Theorem Prover in Prolog written during lecture is now available.
(10/11) Midterm 1 Solutions are available.
(10/4) Solutions are now available for Assignment 5.
(10/4) Solutions are now available for Assignment 4.
(09/27) Solutions are now available for Assignment 3.
(09/20) Solutions are now available for Assignment 2.
(09/13) Solutions are now available for Assignment 1.
(9/1) Tutch problems done in recitation are available.

Class Material

Schedule	Lecture schedule, readings, and code
Assignments	Assignments, due dates, and policies
Handouts	Course handouts
Software	Proof checkers, language implementations, model-checkers

Course Information

Lectures	TuTh 12:00-1:20, GHC 4102, Karl Crary
Recitations	Section A, Wed 12:30-1:20, WeH 4623, Chris Martens
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	Thursday 5-6pm	x8-7687	crary@cs
Teaching Assistant	Chris Martens	GHC 9005	Wednesday 3-4pm	x8-5940	cmartens@cs

[ Home | Schedule | Assignments | Software ]