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.
Lectures: Mon-Wed 16:30 ~ 17:50 (CMB 2147)
Recitations: Thu 09:30 ~ 10:20 (CMB 2147)
Piazza: Gradescope (entry code will be posted on piazza): https://gradescope.com/courses/5861
Instructor: Giselle Reis
Office: CMU-Q 1008
Office hours: by appointment
– Due on Mondays before class, i.e, 16:29.
– May contain written and programming parts.
– To be solved individually unless explicitly stated.
– Evaluated on the basis of correctness, clarity and elegance (no typos and no bad grammar).
– Asking and answering questions and contributing to discussions in class.
– Participating on discussions on Piazza.
– Using LaTeX for assignments.
– Attending recitations.
Midterm I: 15%
Midterm II: 15%
Final exam: 25%
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.
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 firstname.lastname@example.org . 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.