This language implementation is designed to accompany four lectures at OPLSS during Summer 2023. Notes for these lectures are included in the distribution:
(The documentation README.md includes details about how the notes are typeset.)
These lecture notes correspond to an increasingly expressive demo implementation of a dependently-typed lambda calculus. Each of the following subdirectories is a self-contained implementation and all are generated from the same source, located in the main/ directory.
- version1/: Basic language implementation
- version2/: Basic language extended with nontrivial definitional equality
- version3/: Above, extended with irrelevant arguments
- full/: Full language with datatypes
The implementation README.md includes instructions about how to compile and work with these implementations. Edits should only be for versions in the main/ directory.
There is a VS Code plugin for pi-forall.
This is a revised version of lecture notes originally presented at OPLSS during 2023, 2022, 2014, and 2013.
Videos from the 2022 and 2014 lectures are available from the OPLSS website. If you watch these videos, you should look at the corresponding branch of this repository. Unfortunately, the 2023 recordings include only audio, and only for part of the lectures.
An abridged version of these lectures was also given at the Compose Conference, January 2015. Notes from this version are also available.
-- Stephanie Weirich