@zyang wow! this is really cool! I'm working on a language that has an explicit substitution operation whose semantics is a free monad (ie see the paper Explicit Substitutions and Higher-Order Syntax by Neil Ghani), do you think your technique would be applicable to it?
for technical reasons I'm forced to use small-step operational semantics rather than nbe, so if substitution could be made more efficient I would be extremely interested!
=> More informations about this toot | View the thread | More toots from zanzi@mathstodon.xyz
=> View zyang@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).