[racket] Does Redex have support for multi-hole evaluation contexts?

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 <lkuper at cs.indiana.edu> wrote:
> On Mon, Jul 9, 2012 at 12:11 PM, Ryan Newton <rrnewton at 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