Redex

A great way to experiment with semantics, including reduction relations (roughly, the part of the semantics that says how the program runs) and type systems.