Robbert Krebbers authored
We can use a named representation because we only substitute closed values. This idea is borrowed from Pierce's Software Foundations. The named representation has the following advantages: * Programs are much better readable than those using De Bruijn indexes. * Substitutions on closed terms (where all variables are explicit strings) can be performed by a mere simpl instead of Autosubst's asimpl. The performance of simpl seems better than asimpl. * Syntactic sugar refolds better.eba4ac6e
To learn more about this project, read the wiki.