在 pi-forall 中实现依赖类型
Implementing Dependent Types in pi-forall
AI总结：
本讲义介绍最小依赖类型语言 pi-forall 的设计及其类型检查器实现，源自2023年俄勒冈编程语言暑期学校课程。
摘要：
这些课程讲义描述了名为“pi-forall”的最小依赖类型语言的设计，并逐步介绍其类型检查器的实现。它们基于2023年7月在俄勒冈编程语言暑期学校讲授的课程。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
