For Macro Lovers: Tauto and the World's Most Powerful Macro System

Hygienic DSLs, typed transformations, proof tactics, and effect-restricted expansion in one macro system.