2024 Faculty Courses School of Computing Department of Mathematical and Computing Science Graduate major in Mathematical and Computing Science
Topics in Algebra
- Academic unit or major
- Graduate major in Mathematical and Computing Science
- Instructor(s)
- Shunsuke Tsuchioka
- Class Format
- Lecture (Face-to-face)
- Media-enhanced courses
- -
- Day of week/Period
(Classrooms) - 7-8 Mon / 7-8 Thu
- Class
- -
- Course Code
- MCS.T417
- Number of credits
- 200
- Course offered
- 2024
- Offered quarter
- 4Q
- Syllabus updated
- Mar 14, 2025
- Language
- Japanese
Syllabus
Course overview and goals
Understanding dependent types and formal proofs via an implementation of a verifier
Course description and aims
(1) implementation of a verifier based on the textbook "Type Theory and Formal Proof: An Introduction by R. Nederpelt and G. Geuvers" in a programming language such as C, python, etc.
(2) formal proof by using your verifier of simple propositions
(3) theoretical background will not be explained because I put emphasis on implementation in the course
Keywords
lambda cube, formal proof, dependent types
Competencies
- Specialist skills
- Intercultural skills
- Communication skills
- Critical thinking skills
- Practical and/or problem-solving skills
Class flow
Mondays will be for explaining the textbook. Thursdays will be exercise-style implementation time.
Course schedule/Objectives
| Course schedule | Objectives | |
|---|---|---|
| Class 1 | introduction | Understand the content of the class |
| Class 2 | implementation (alpha equivalence) | Understand the content of the class |
| Class 3 | lambda cube | Understand the content of the class |
| Class 4 | implementation (beta reduction) | Understand the content of the class |
| Class 5 | descriptive definitions (alias) | Understand the content of the class |
| Class 6 | implementation (delta conversion) | Understand the content of the class |
| Class 7 | primitive definitions (axioms) | Understand the content of the class |
| Class 8 | implementation (type inference) | Understand the content of the class |
| Class 9 | implementation (complexity) | Understand the content of the class |
| Class 10 | de Bruijn index | Understand the content of the class |
| Class 11 | implementation (optimization) | Understand the content of the class |
| Class 12 | propositions-as-types (proofs-as-terms) correspondence (PAT) | Understand the content of the class |
| Class 13 | proof assistant (Lean) | Understand the content of the class |
| Class 14 | A future of mathematics? (IMHO) | Understand the content of 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)
「Type Theory and Formal Proof: An Introduction (by R. Nederpelt and H. Geuvers) 」, Cambridge University Press (viewable at Tokyo Tech)
Reference books, course materials, etc.
I will open a course webpage and upload supplementing materials
Evaluation methods and criteria
Based on your implementation (source code) and comprehension checks
Related courses
- MTH.A301 ： Algebra I
- MTH.A302 ： Algebra II
- MTH.A331 ： Algebra III
Prerequisites
(1) I require that you can write a simple code in one or more programming languages (mandatory)
(2) You can execute my binary for reference if you have a C++ compiler (not mandatory)
(3) I only require that you are familiar with elementary mathematics (high school level, not undergraduate level)