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.
