Home
Schedule
Assignments
Software
 
Course Profile
 
Piazza
Gradescope
 
fp@cs
Frank Pfenning
  

15-317 / 15-657 Constructive Logic

Spring 2023
Frank Pfenning
TuTh 8:00-9:20
TEP 1403
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 program 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

Lectures Tue Thu 8:00am-9:20am, TEP 1403
Recitations Section A, Wed 8:00am-8:50am, WEH 2302, Sophia Roshal
  Section B, 10:00am-10:50am, WEH 2302, Luiz de Sa
  Section C, 11:00am-11:50am, POS 145, Shengchao Yang
Office Hours Frank Pfenning, Wed 11:30am-1:00am, GHC 6017
  Shengchao Yang, Mon 5:00pm-6:00pm, GHC 5th Floor, Carrel 2
  Luiz de Sa, Tue 10:00am-11:30am, GHC 5005
  Sophia Roshal, Thu 2:30pm-4:00pm, GHC 6023
  Jonathan Ho, Mon 6:30pm-8:00pm, GHC 5th Floor Citadel Commons
and Thu 4:00pm-5:30pm, GHC 5th Floor Citadel Commons
Course Communication piazza.com/cmu/spring2023/15317
Notes There is no textbook, but lecture notes will be posted
Credit 9 units
Grading 45% Homework, 15% Midterm, 15% Miniproject, 25% Final
Grade Cutoffs A: ≥ 90%, B: ≥ 80%; C: ≥ 70%; D: ≥ 60%
Grade ranges may be lowered slightly based on difficulty of assignments and exams
Homework Homework is assigned weekly and handed in via Gradescope
You have 5 late to use throughout the semester
If you need more than 2 late days on a given assignment, you need to notify the instructor
Midterm Exam Thu Mar 2, in class.
Closed book, closed notes.
Miniproject Checkpoint: Apr 4, Final: Apr 11
Final Exam Tue May 2, 5:30pm-8:30pm, DH 1212-1211-1209
Closed book, closed notes.
Home http://www.cs.cmu.edu/~fp/courses/15317-s23/

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

  • define logical connectives and test these definitions for harmony
  • develop sound and complete theorem provers based on deductive presentations of logics
  • derive operational interpretations of logics via proof reduction and use them to write correct programs
  • derive operational interpretations of logics via proof search and use them to write correct programs

Topics: Some of these topics are tentative, depending on the pace of the course and participant interests.

  • Natural deduction
  • Harmony
  • Proofs as programs
  • Quantification
  • Induction and primitive recursion
  • Sequent calculus
  • Cut elimination
  • Inversion
  • Theorem proving
  • Backward logic programming; Prolog
  • Forward logic programming; Datalog
  • Polarization and focusing
  • Linear logic
  • Classical logic

Prior Versions of This Course

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.

[ Home | Schedule | Assignments | Resources ]

fp@cs
Frank Pfenning