We have several papers proposing denotational semantics for various PP formalisms. It would be good to be able to compare them. Here’s a challenge to the authors of these papers:
For your semantics, please give a few examples of each of the following:
- interesting equivalences between open terms that are equated in your semantics. These should include both equivalences that are expressible in other formalisms, and those that are particular to the language that you are modeling.
- interesting equivalences between open terms that are not equated in your semantics. Please explain why you believe these pairs of terms should be equivalent, and why they are not equated by your semantics.
- terms that are equated in your semantics, but perhaps should not be considered equivalent (if any).
You can do this in the comments or as new posts, or at worst, in your posters.
Having these examples in hand will enable us to have much more fruitful discussions about the various proposed semantics.
Looking forward to a fun discussion,