Implementing Dependent Types in pi-forall
Programming Languages
2023-07-13 v2
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.
Keywords
Cite
@article{arxiv.2207.02129,
title = {Implementing Dependent Types in pi-forall},
author = {Stephanie Weirich},
journal= {arXiv preprint arXiv:2207.02129},
year = {2023}
}
Comments
54 pages