A toy interpreter for a Scheme-like language
An STG-like lazy evaluation mechanism
Generates LaTeX derivation trees for LK sequents