CMU 15-317: Constructive Logic (Fa'15)

15-317 Constructive Logic (Fall 2015)

Instructor:	André Platzer (office: Thu 4-5:00, GHC 9103)
Teaching Assistants:	Anna Gommerstadt hgommers@andrew (office: Mon 5-6:30, GHC 9219) Vincent Huang vincenth@andrew (office: Fri 4:30-6:00, GHC carrel) Michael Coblenz mcoblenz@andrew (office: Mon 3:30-5, GHC 7121)
Units:	9
Semester:	Fall 2015
Time:	TR 1:30-2:50
Place:	WeH 5403
Recitation:	A: W 11:30-12:20 GHC 5222, Anna Gommerstadt B: W 12:30-1:20 GHC 5222, Vincent Huang C: W 4:30-5:20 GHC 4211, Michael Coblenz
	This course is listed in the Computer Science Department as 15-317/15-657 at Carnegie Mellon University. It counts as a Logics/Languages elective in the Computer Science curriculum.

Questions
Schedule

DESCRIPTION:

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.

PREREQUISITES:

15-150: Functional Programming.

TEXTBOOK:

There is no textbook.

METHOD OF EVALUATION:

Grading will be based on a set of homework assignments and exams. 40% Assignments, 15% Midterm I, 15% Midterm II, 30% Final.

Midterm I:	Thu 10/01 during lecture time, 150 points. Closed book, one double-sided sheet of hand-written notes permitted.
Midterm II:	Tue 11/10 during lecture time, 150 points. Closed book, one double-sided sheet of hand-written notes permitted.
Final:	Thu 12/17, 5:30-8:30, DH A302, 300 points. Open book.

MORE INFORMATION:

See prior instances of this course by Frank Pfenning, Karl Crary and Penny Anderson as well as Iliano Cervesato for more information on prior versions of this course.