I encourage you to give K a try and report back how things go and/or even compare things a little (for the purposes of improving the tools, of course).
Also, and I realize that it is a bit late, but there's this if you want to get some help getting started on a bunch of such things: https://fmse.info.uaic.ro/events/SSLF12/ Robby On Mon, Jul 9, 2012 at 3:13 PM, Lindsey Kuper <lku...@cs.indiana.edu> wrote: > On Mon, Jul 9, 2012 at 12:11 PM, Ryan Newton <rrnew...@gmail.com> wrote: >> We felt it was necessary to include simultaneous steps (Matthias's [A] >> scenario) to model real parallel machines and force us to deal with >> potentially incompatible simultaneous updates to the store. >> >> Lindsey had a slightly awkward time shoehorning things into redex, and the >> resulting model runs pretty slowly. BUT, these are just nits and possible >> areas for improvement. Redex was still enormously helpful and fulfilled its >> purpose. There wasn't any existential crisis here. > > Yep. Although, as Matthias pointed out, Redex is ill-suited for > modeling simultaneous steps, it has *still* been quite helpful in > clarifying our thinking and exposing bugs, even though we weren't able > to take advantage of most of what it has to offer. Having said that, > there must be semantics engineering tools that are better suited for > modeling truly simultaneous reductions (the K system comes to mind as > a possibility, although I haven't tried it yet). But the > lightweight-ness of Redex is pretty hard to beat. (It's also > enormously fun.) > > Lindsey ____________________ Racket Users list: http://lists.racket-lang.org/users
