| |
15-317 / 15-657 Constructive Logic
| Spring 2022 |
| Instructor: Klaas Pruiksma |
| Teaching Assistants: Runming Li, Onyekachi Onyeador, Viraj Puri, Xiao Yu |
| Tuesday, Thursday 08:35-09:55 |
| POS A35 |
| 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 08:35-09:55, POS A35
(Also available online, at this Zoom link)
|
| Recitations |
Section A, 09:05-09:55, PH A18C, Runming Li
|
| |
Section B, 10:10-11:00, DH 1211, Onyekachi Onyeador
|
| |
Section C, 11:15-12:05, DH 2105, Viraj Puri
|
| Office Hours |
Tuesday 16:00-18:00 (Gates 5th Floor Commons, Table 1)
|
| |
Wednesday 17:00-19:00 (Gates 5th Floor Commons, Table 4)
|
| |
Thursday 17:00-19:00 (Zoom link, passcode 934389)
|
| |
Sunday 16:00-18:00 (Zoom link)
|
| Course Communication |
http://piazza.com/cmu/spring2022/15317 |
| Notes |
There is no textbook, but lecture notes will be posted
|
| Credit |
9 units |
| Grading |
40% Homework, 30% Midterms, 30% Final |
| Grade Cutoffs |
A: ≥ 90%, B: ≥ 80%; C: ≥ 70%; D: ≥ 60%
Grade ranges may be lowered slightly based on difficulty of homeworks and exams
|
| Homework |
Homework is assigned weekly and handed in via Gradescope.
You have 5 late to use throughout the semester,
with at most 2 late days on any given assignment.
|
| Midterm I |
Tue Feb 22, in class.
One sheet of notes allowed.
|
| Midterm II |
Tue Apr 5, in class.
One sheet of notes allowed.
|
| Final |
Location and time TBD
One sheet of notes allowed.
|
Learning objectives:
After taking this course, students will be able to
- understand the distinction between classical
and constructive logic.
- define logical connectives and test these
definitions for harmony.
- express and prove the relationships between
different presentations of a logic (e.g. natural
deduction and sequent calculus) and explain why
one presentation might be preferred over another.
- 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
- understand the applications of substructural and
modal 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.
[ Home
| Schedule
| Assignments
| Software
]
|