15-317: Constructive Logic (Spring 2019)

This course is designed to be a thorough introduction to constructive (also called intuitionistic) logic. It assumes no previous knowledge of formal logic, starting from the building blocks that are actually used for any logic: connectives, formulas, propositions, judgments and proof calculi. After formalizing constructive logic, we see its relation to computation via the Curry-Howard isomorphism (formulas-as-types, proofs-as-programs) and logic programming (formulas-as-programs). The course ends by showing how to increment and modify this logic in order to increase its expressiveness.

Learning goals


This is a 9 unit course.

Place and time

Mondays and Wednesdays 16:30 to 17:50 CMB 2147 lectures
Thursdays 08:30 to 09:20 CMB 2147 recitations



Giselle Reis (Instructor)

Office: 1008
Office hours: by appointment
E-mail: giselle@cmu.edu

Tamim Jabban (TA)

Office: 1004
Office hours: by appointment
E-mail: tamim@cmu.edu



Homework: 40%

Exam I: 15%
Exam II: 15%
Final exam: 30%

Getting the Assignments

The writeup and starter files for each assignment can be found on the schedule above.

Submitting the Assignments

You need to submit a pdf file containing your solutions to Gradescope.


You are expected to comply with the university policy on academic integrity (see also The Word and Understanding Academic Integrity).

Collaboration is regulated by the whiteboard policy: you can bounce ideas about a homework with other students, but when it comes to typing it down for submission, you are on your own. You are not allowed to use notes, files, pictures, etc, from any previous discussion nor previous versions of this course.

We will run a program that detects code similarity on all your homework submissions. If students are found to have submitted almost the same code, they will be contacted and this may result on an academic integrity violation report.

An Invitation to Students with Learning Disabilities:

Carnegie Mellon University is committed to providing reasonable accommodations for all persons with disabilities. To access accommodation services you are expected to initiate the request and submit a Voluntary Disclosure of Disability Form to the office of Health & Wellness or CaPS-Q. In order to receive services/accommodations, verification of a disability is required as recommended in writing by a doctor, licensed psychologist or psycho-educational specialist. The office of Health & Wellness, CaPS-Q and Office of Disability Resources in Pittsburgh will review the information you provide. All information will be considered confidential and only released to appropriate persons on a need to know basis.

Once the accommodations have been approved, you will be issued a Summary of Accommodations Memorandum documenting the disability and describing the accommodation. You are responsible for providing the Memorandum to your professors at the beginning of each semester.

Take Care of Yourself:

Do your best to maintain a healthy lifestyle this semester by eating well, exercising, getting enough sleep and taking some time to relax. This will help you achieve your goals and cope with stress.

All of us benefit from support during times of struggle. You are not alone. 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 often 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-Q) is here to help: call 4454 8525 or make an appointment to see the counselor by emailing student-counselling@qatar.cmu.edu. Consider reaching out to a friend, faculty or family member you trust for help.

If you or someone you know is feeling suicidal or in danger of self-harm, call someone immediately, day or night at 5554 7913. If the situation is life threatening, call 999.