Now reading the Redex book (thank you, @spdegabrielle!)—slowly but surely. I really like that it starts from the roots. If I have some suggestions for improvement for a potential next version, who should I send the feedback to?

Matthias

I did that a couple of times

(though it turned out I was misunderstanding for most of them lol)

One thing that’s bothering me a little is what meaning can we assign to "=", in particular in the definition of the substitution function in page 26? Is this equality some ‘meta’-level language, or is this equality the compatible, reflexive, symmetric, transitive closure of a (yet not precisely defined) relation?

I expect that too :wink:

The = in those definition is part of the relation-defining notation (so, meta-level in that sense). That kind of = also appears in the second and third boxes of section 1.6.

What’s the full title of the Redex book? I’m pretty sure somebody recommended it during PLMW @ ICFP yesterday.

“Semantics Engineering with PLT Redex”

Thanks :slightly_smiling_face:

It was mentioned in David van Horn’s talk on operational semantics. A couple of us typed out the name and authors in the chat window!

Oh right :+1::skin-tone–2: Must have missed those comments :stuck_out_tongue: