HackerPapers

arXiv:2207.02129cs.PL

Implementing Dependent Types in pi-forall

Stephanie Weirich

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

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.

arXiv comments
54 pages
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

No comments linking this paper were found in the collected sources. Found in 2 HN submissions from Jul 2022 to Jun 2025. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.