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 < > mallku...@gmail.com> 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 racket-users...@googlegroups.com. >> 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com.
