Skip to content

sweirich/pi-forall

2022
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
doc
 
 
 
 
 
 
old
 
 
 
 
 
 
 
 
 
 
 
 
 
 

pi-forall language

This language implementation is designed to accompany four lectures at OPLSS during Summer 2022. 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 dependently-typed lambda calculus. Each of the following subdirectories is self-contained (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.

History

This is a revised version of lecture notes originally presented at OPLSS during 2014 and 2013.

Videos from the 2014 lectures are also available from the OPLSS website. If you want to watch these videos, you should look at the 2014 branch of this repository.

An abridged version of these lectures was also given at the Compose Conference, January 2015. Notes from this version are also available.

  • compose.md: Overview of pi-forall implementation

-- Stephanie Weirich

About

A demo implementation of a simple dependently-typed language

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published