Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

I have no experience with Redex (it is one of the things I want to get more familiar with in the future), but I happened to watch this talk: "Finding bugs without running or even looking at code" by Jay Parlar https://www.youtube.com/watch?v=FvNRlE4E9QQ Maybe a tool like this is interesting to

Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

> On Nov 9, 2019, at 09:18, Jay McCarthy wrote: > > "remember that an evaluation context is just a way of describing more > succinctly what you could otherwise define by hand as a big, > complicated relation on individual terms." Yes, that makes sense — I wasn’t really considering what it would

Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

That is an interesting idea. I want to emphasize this point again: "remember that an evaluation context is just a way of describing more succinctly what you could otherwise define by hand as a big, complicated relation on individual terms." There is nothing special about evaluation contexts. I

Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

I am not sure how the details work out but I guess Jay's advice of writing a judgement form that shows how terms reduce is the right thing (and that judgment form may or may not use context decomposition patterns). Robby On Sat, Nov 9, 2019 at 6:31 AM Alexis King wrote: > Hi Jay, > > I

Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

Hi Jay, I appreciate your pointers! However, I think either I didn’t make my question clear enough, or I misunderstand your explanation (or perhaps some of both). What I am trying to model is, indeed, a form of delimited control. I have already written a model that supports a couple classic

Re: [racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

First, any inductive definition could be defined with `define-judgment-form` (although derivations will only be discoverable if you can give a mode spec.) If the semantics you're talking about can't be written as an inductive definition, then it probably doesn't make any sense. Second, remember

[racket-users] Modeling a context-sensitive evaluation context with PLT Redex?

Hello, I am trying to model a (not quite algebraic) effect system in PLT Redex, but I’m struggling to encode my evaluation contexts into Redex’s pattern language. My question is best explained via example, so I’ll start with a bog-standard call-by-value lambda calculus: (define-language