Lambda the Ultimate

I was reading Pierce, and was also toying with some type-system thoughts I'd had, and the idea working out a formal representation of such seemed like a fun deal, but rather than scribbling on paper, I was wondering if anyone knew of any sort of workbench/toolkit out there that existed for this sort of purpose. Something where you can enter terms and watch it go, see if you hit stuck states, etc. This'd be a magnificent boon to students, but I haven't heard of anything like this (I suppose this may simulable with coq or other sorts of high-power "expert-friendly" toolsets, but I haven't seen the "newbie-friendly" variant thereof...).

Has anyone heard of anything like this?