This language implementation is designed to accompany four lectures at OPLSS during Summer 2014. Notes for these lectures are included in the distribution:
- notes.md: Basic language with Type:Type
- notes2.md: Implementation of basic languages
- notes3.md: Definitional and propositional equality
- notes4.md: Datatypes, with parameters and indices, erased arguments
Videos for these lectures are also available from the OPLSS website.
These lecture notes corresponds to an increasingly expressive demo implementation of dependently-typed lambda calculus.
- version1/: Basic language implementation,
- version2/: Basic language extended with nontrivial definitional equality
- soln/: Full language with datatypes and erased arguments
See also the implementation README.md for more details.
All of these versions are excerpted from the marked up files in the directory:
All edits should be to the code in the
master directory. The above versions
are included in the repo just for convenience.
-- Stephanie Weirich, June 2014