also me. I will be reading all thesis.
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Conversation
once I approached Simon Gay and said: I read your undergraduate thesis.
1
4
oh wow, I'd be shocked if someone read mine.
1
2
I’mma add Liam’s to the pipeline as of today 😂
1
4
I think my undergrad thesis has some good stuff mixed in with some cringey stuff, so it's available publicly but not publicised anywhere. There is one nice technique I invented that I haven't seen anywhere else though..
1
3
(Basically, the technique is, if you're formalising some algorithmic rules like a constraint generator or elaboration rules that rely on generating "fresh" unification variables, don't do that. Put an actual binder for the variable into the structure of your output and then...
2
6
shift the binders up as far as possible. The shifting can handle the de bruijn shifting or whatever is needed to make sure the names stay unique thus guaranteeing "fresh"ness)
2
3
This sounds like some things you run into when elaborating dependent pattern matching… not sure I'll be able to use this when I get to it next, but it seems handy! I think went with a fresh name generator in Sixty?
Yes: Sixty does NbE with De Bruijn indices in the syntax and fresh vars in the domain to avoid shifting during pattern matching elaboration, which can make modifications to the middle of the context. But I guess implementations might have different tradeoffs than formalisations.
1
1
Assuming that the implementations and formalisations are distinct... :)