Topics in algebra（4Q, Mon and Tue, 7-8）

• Date：4Q, Mon and Tue, 7-8（15:25-17:05）
• Room：W83?
• Textbook：Type Theory and Formal Proof and Errata（by Rob Nederpelt and Herman Geuvers, Cambridge University, available in the university）
• Evaluation： By implementations, the formal proofs (= lambda terms) you actually write, and the presentation.
• The content of this class is not directly related to algebra in pure mathematics.
• The classes for 2025 Dec 8 (Mon)+11 (Thur) and 2026 Jan 19+26 (Mons) will be cancelled.
• In the final day (not determined yet), I will require you to give a short presentation on your implementation.
• In the first half of the class we will implement a type verifier, and then we will implement a type inferencer.
• We will conduct the course in the same manner as in the 2023 academic year. Details can be found here.

• Your browser may be reading its cache, so please reload when viewing this page.