CMU 15-317: Constructive Logic (Sp'21)

15-317 Constructive Logic (Spring 2021)

Instructor:	André Platzer (office hour: Tue 16:30-17:30)
Teaching Assistants:	Akshina Gupta akshinag@andrew, OH Sun 16:00-17:00 Julia Gu juliag1@andrew, OH Mon 15:00-16:00 Ethan Rosenthal emrosent@andrew, OH Tue 20:30-21:30 Avery Cowan acowan@andrew, OH Wed 16:00-17:00 Zhibo Chen zhiboc@andrew, OH Thu 16:30-17:30
Units:	9
Semester:	Spring 2021
Time:	TR 8:20-9:40 CMU Remote
Recitation:	A: W 9:10-10:00 CMU Remote, Julia Gu B: W 10:30-11:20 CMU Remote, Ethan Rosenthal C: W 11:40-12:30 CMU Remote, Zhibo Chen D: W 15:00-15:50 CMU Remote, Avery Cowan E: W 19:00-19:50 CMU Remote, Akshina Gupta
	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 Piazza Gradescope

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 with a minimal grade of C.
For the cross-listed graduate version, 15-657, experience with functional programming is recommended.

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:	Tue 03/09 during lecture time, 150 points.
Midterm II:	Tue 04/06 during lecture time, 150 points.
Final:	Tue 05/11 during finals week, 300 points.

MORE INFORMATION:

See prior instances of this course in Fall 2015 and Fall 2016 and Spring 2020 and by Frank Pfenning, Karl Crary for more information on prior versions of this course.