15-317 / 15-657 Constructive Logic

Fall 2024

Instructor: Karl Crary

Teaching Assistants: Jonathan Ho, Aresh Pourkavoos, Emily Song

Mon and Wed, 11am - 12:20pm

HH B131

9 units

This undergraduate course provides an introduction to constructive logics, such as intuitionistic and linear logic, with an emphasis on their application in computer science. This includes basic means for defining logics (for example, natural deduction and sequent calculus), establishing properties of logics (for example, cut elimination), and for investigating their computational interpretations (for example, via proof reduction or proof search).

Prerequisites: 15-317 is an introductory undergraduate course with a minimum grade of C in 15-150 as prerequisite. For the cross-listed graduate version, 15-657, some experience with functional programming is recommended.

Class Material

Schedule	Lecture notes and additional readings
Assignments	Homeworks assignments and due dates
Software	Links to software and other resources

Course Information

Syllabus	here
FAQ	here
Recitations	Section A, Tue, 9am - 9:50am, DH 2122
	Section B, Tue, 10am - 10:50am, POS 147
	Section C, Tue, 11am - 11:50am, GHC 4211
	Section D, Tue, 12 noon - 12:50pm, Wean 4707
Office hours	Mon, 5pm - 6pm (Ho), GHC 5th floor
	Wed, 5:30pm - 6:30pm (Song), GHC 5th floor
	Thu, 6pm - 7pm (Pourkavoos), Wean 6403
	Fri, 3:30pm - 4:30pm (Crary), GHC 9217
	Office hours times and locations are subject to change.
Piazza page	here
Grading	48% homework, 19% midterms, 29% final, 4% attendance
Textbook	Lecture notes are effectively the course textbook.
Homework	Homework is assigned weekly and handed in via Gradescope. See the syllabus for the late day and collaboration policies.
Exams	Open one-sheet-of-notes, closed internet.

Learning objectives: After taking this course, students should be able to:

understand the distinction between classical and constructive logic, and the uses of constructive logic
define logical connectives and test these definitions for harmony
express and prove the relationships between different representations of a logic (e.g., natural deduction and sequent calculus), and explain what each representation is for
implement propositional theorem provers
use operational interpretations of logics via proof search (a.k.a. logic programming)
understand the applications of substructural logics

Accommodations for Students with Disabilities

If you have a disability and have an accommodations letter from the Disability Resources office, I encourage you to discuss your accommodations and needs with me as early in the semester as possible. I will work with you to ensure that accommodations are provided as appropriate. If you suspect that you may have a disability and would benefit from accommodations but are not yet registered with the Office of Disability Resources, I encourage you to contact them at access@andrew.cmu.edu.

Support for Students' Health and Well-Being

All of us benefit from support during times of struggle. There are many helpful resources available on campus and an important part of the college experience is learning how to ask for help. Asking for support sooner rather than later is almost always helpful. If you or anyone you know experiences any academic stress, difficult life events, or feelings like anxiety or depression, we strongly encourage you to seek support. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website at http://www.cmu.edu/counseling/. Consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.

The Scientific American article referenced in the syllabus.

[ Home | Schedule | Assignments | Software ]