These lecture notes describe the design of a minimal dependently-typed language called "pi-forall" and walk through the implementation of its type checker. They are based on lectures given at the Oregon Programming Languages Summer School during July 2023.

翻译：这些讲义描述了一个名为“pi-forall”的最小依赖类型语言的设计，并逐步介绍了其类型检查器的实现。内容基于2023年7月在俄勒冈编程语言暑期学校讲授的课程。