Home » forums » LtU Forum

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?

By jimdesu at 2010-11-11 01:42 | LtU Forum | previous forum topic | next forum topic | other blogs | 4363 reads

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.

By Lauri Alanko at Thu, 2010-11-11 04:41 | login or register to post comments

thanks

I'll check it out. :)

By jimdesu at Thu, 2010-11-11 05:53 | login or register to post comments

OTT

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

By fredokun at Fri, 2010-11-12 10:23 | login or register to post comments