Binders unbound
Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution seem simple, yet subtle bugs often go undetected....
Main Authors: | , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
ACM
2011
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.401.2651 http://www.cis.upenn.edu/~byorgey/pub/unbound.pdf |