2024 Faculty Courses School of Computing Department of Mathematical and Computing Science Graduate major in Mathematical and Computing Science
Logic and Computation
- Academic unit or major
- Graduate major in Mathematical and Computing Science
- Instructor(s)
- Ryo Kashima
- Class Format
- Lecture (Face-to-face)
- Media-enhanced courses
- -
- Day of week/Period
(Classrooms) - 3-4 Mon / 3-4 Thu
- Class
- -
- Course Code
- MCS.T416
- Number of credits
- 200
- Course offered
- 2024
- Offered quarter
- 4Q
- Syllabus updated
- Mar 14, 2025
- Language
- English
Syllabus
Course overview and goals
This course covers the intersection of programming language theory and mathematical logic.
The key notion is "Curry-Howard correspondence", which shows the direct relationship between computer programs and mathematical proofs.
Topics include syntax and semantics of classical and intuitionistic logics, various proof systems (natural deduction, sequent calculus, etc.), and lambda calculus (Church–Rosser theorem, type-free and typed lambda calculus, strong normalization theorem, etc.).
Course description and aims
Students will acquire an insight into the logical foundations of computation.
Keywords
classical logic, intuitionistic logic, natural deduction, sequent calculus, Kripke model, Curry-Howard correspondence, type-free and typed lambda calculus, Church–Rosser theorem, strong normalization theorem, combinatory logic.
Competencies
- Specialist skills
- Intercultural skills
- Communication skills
- Critical thinking skills
- Practical and/or problem-solving skills
Class flow
The course consists of lectures.
Students will have exercise assignments several times.
Course schedule/Objectives
| Course schedule | Objectives | |
|---|---|---|
| Class 1 | Truth, validity, and satisfiability of logical formulas. | Instructed in the class. |
| Class 2 | Natural deduction. | Instructed in the class. |
| Class 3 | Sequent calculus. | Instructed in the class. |
| Class 4 | Cut-elimination theorem and completeness theorem. | Instructed in the class. |
| Class 5 | Intuitionistic logic (1). | Instructed in the class. |
| Class 6 | Intuitionistic logic (2). | Instructed in the class. |
| Class 7 | Normalization of proofs in natural deduction. Combinatory logic (1). | Instructed in the class. |
| Class 8 | Introduction to lambda calculus. | Instructed in the class. |
| Class 9 | Combinatory logic (2). Arithmetic by lambda calculus. | Instructed in the class. |
| Class 10 | Church–Rosser theorem. | Instructed in the class. |
| Class 11 | Left-most reduction theorem. Simply typed lambda calculus. | Instructed in the class. |
| Class 12 | Curry-Howard correspondence. | Instructed in the class. |
| Class 13 | Strong normalization theorem. | Instructed in the class. |
| Class 14 | Second-order typed lambda calculus. | Instructed in the class. |
Study advice (preparation and review)
To enhance effective learning, students are encouraged to spend approximately 100 minutes preparing for class and another 100 minutes reviewing class content afterwards (including assignments) for each class.
They should do so by referring to textbooks and other course material.
Textbook(s)
Dirk van Dalen: Logic and Structure, Fourth Edition (Corrected 2nd printing 2008).
Henk Barendregt, Erik Barendsen: Introduction to Lambda Calculus (Revised edition December 1998, March 2000).
Reference books, course materials, etc.
Instructed in the class.
Evaluation methods and criteria
Based on exercise assignments.
Related courses
- MCS.T313 ： Mathematical Logic
Prerequisites
Students who had completed MCS.T404 "Logical Foundations of Computing" cannot take this course.