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....

Full description

Bibliographic Details
Main Authors: Stephanie Weirich, Brent A. Yorgey, Tim Sheard
Other Authors: The Pennsylvania State University CiteSeerX Archives
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