HTTPS SSH

Pi-Forall language

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