Namely, Painless

This book presents a novel approach to safe meta-programming. A meta-program is a program which processes programs or similar data. Compilers and theorem provers are prime examples of meta-programs which could benefit from this approach. To this end, this work focuses on the representation of names and binders in data structures. Our technique is demonstrated on several examples including normalization by evaluation which is known to be challenging. We show that our world-indexed approach can express a wide range of data types by embedding several definition languages from the literature.