Implementations of various lambda calculi and type systems, mostly from Harper's PFPL. Including:
Done
- Goedel's System T (Simply Typed Lambda Calculus)
- Language with a control stack and call-cc
Todo:
- System F
- Plotkin's PCF
- System T with Bidirectional Type Checking
- Hindley-Milner type system
- Substructual type systems
- Linear, affine, ordered