I'm sorry, my sentence was ambiguous! I'm saying that I don't know of any other work that is specifically focused on the semantics of Redex. (Of course, there may be work I'm not aware of.)
The paper is still a good match, I believe, yes. You're right that the syntactic checks for well-formed grammars have tightened since that era, but if the program is valid, then I think it should match; the underlying algorithms have not changed, only bug fixes have happened. Of course, if you find that this isn't the case, I'd be very interested to hear more :) Robby On Wed, Dec 8, 2021 at 6:34 PM Mallku Ernesto Soldevila Raffa < [email protected]> wrote: > I beg your pardon!, I'm not understanding the answer, what is it that > might be specific of Redex? > > I suspect that the answer is that there isn't some recent work on formal > semantics specifically about Redex. In that case, does anybody know if the > already mentioned paper [1] is still a good match for today's semantics of > Redex? The paper provides a mechanization of the model in Redex, together > with some tools to test it. Of interest is a tool that asks Redex to > generate > random patterns and terms that match against them, and tests if the > mechanized model is capable of reproducing the matching (or that is what > I suspect that the tests are doing :P ). It was possible to run the > mechanization > on a recent version of Redex, but the generated patterns are ill-formed > (e.g., in-hole p1 p2, where p1 contains more than 1 hole). Of course I > could > provide more details about the error, but I don't know if it is of > interest, it's > a mechanization written for the Redex version that comes with Racket 5.* > or something like that. > > Thanks!, > Mallku > > > [1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 > > El miércoles, 8 de diciembre de 2021 a las 21:03:44 UTC-3, Robby Findler > escribió: > >> I think that might be it specifically about redex, I am sorry to say. >> >> Robby >> >> On Wed, Dec 8, 2021 at 5:28 PM Mallku Ernesto Soldevila Raffa < >> [email protected]> wrote: >> >>> Hi community!, >>> I'm interested in understanding the semantics of PLT Redex, since we are >>> working on a tool >>> to translate fragments of Redex models to Coq. At the moment, we just >>> have a >>> mechanization in Coq of the semantics proposed in a ~10 years old paper >>> [1]. Does >>> anybody know if there is an updated work on formal semantics of Redex? >>> >>> Thanks in advance!, >>> Mallku >>> >>> [1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Racket Users" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com >>> <https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com > <https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdOOxK%3Dwo6B0a2PDzVc86G4%3Dc9b%3DxHc7AqYuBD_4KOc1_Aw%40mail.gmail.com.
