Thanks a lot for the info! If I found any mismatches, I'll report it. Regards, Mallku
El miércoles, 8 de diciembre de 2021 a las 23:32:25 UTC-3, Robby Findler escribió: > 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/14b8b2d5-41e8-4864-b194-e968a2043443n%40googlegroups.com.
