A fresh look at programming with names and binders
Nicolas Pouillard, François Pottier · 2010
A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulations in a safe and natural style has, to a large extent, remained elusive.