Implementing Dependent Types in pi-forall

Abstract

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.

54 pages

Cited by in corpus (1)

• Rebound: Efficient, Expressive, and Well-Scoped Binding