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?

(11/29) Extra credit assignment Homework Twelf now available, with Elf starter code.
(11/29) Homework 10 now available, with Elf starter code.
(11/20) Homework 9 now available, with Elf starter code.
(11/1) G4IP in Prolog from recitation posted.
(11/1) Homework 8 now available, with Elf starter code.
(10/26) Homework 7 now available, with Prolog starter code.
(10/18) Homework 6 now available, with SML starter code.
(10/12) Homework 5 now available.
(9/27) Homework 4 now available.
(9/20) Homework 3 now available.
(9/14) Homework 2 now available.
(9/7) Added a Tutch emacs mode by Evan Cavallo.
(9/6) Homework 1 now available.
(9/5) Website created.

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 ]