term-typing/operational semantics simulator?

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?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

PLT Redex

That sounds very much like PLT Redex.


I'll check it out. :)


I am not sure it can work as a simulator, but I think OTT is quite powerful to encode type systems and operational semantics.