elsa is a small proof checker for verifying sequences of
reductions of lambda-calculus terms. The goal is to help
students build up intuition about lambda-terms, alpha-equivalence,
beta-reduction, and in general, the notion of computation
by substitution.
