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.
- Understand what is a logic;
- Learn how logics are defined;
- Comprehend how logics are used in computer science;
- Develop skills in all types of logics: classical, intuitionistic, linear, etc.
This is a 9 unit course.
Place and time
| Mondays and Wednesdays
|| 16:30 to 17:50
|| CMB 2147
|| 08:30 to 09:20
|| CMB 2147
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
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
Consider reaching out to a friend, faculty or family member you trust
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.