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:

  • Basic language with Type:Type
  • Implementation of basic languages
  • Definitional and propositional equality
  • 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 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