|
|
|
|
|
|
by peterbb_net
729 days ago
|
|
|
Nice paper on an interesting topic. I’ve not had a chance to read the paper thoroughly, but the judgmental equality ended up weaker than I anticipated. I’d hope we’d end up with alpha-equivalent codefs being judgmentally equal. Which makes me wonder what the next steps for a proof assistant based on this is. Will the de-/refunctionalization play an active role in the proof assistant as well, thus solving it as described in section 4.1? |
|
|