Where I report on the difficulties presented by the treatment of η-conversion in the setting of the MetaCoq project, try and give insight on why the situation is surprisingly thorny in that specific setting, and consider what we could do to get out of this.
Presentation of our TOPLAS article in the journal-first track of POPL.
Short presentation of work in progress on our TOPLAS article.
Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.