Abstract

Current nominal systems for safely manipulating values with names, like Pure FreshML, only support simple binding structures for those names. As a result, few tools exist to safely manipulate code in those languages for which name problems are the most challenging. We address this by applying those nominal techniques to a richer specification system, inspired by attribute grammars. Our system has the expressive power of David Herman’s λm, but is a full-fledged programming system for any kind of metaprogramming. We demonstrate our system first by implementing it in a core calculus we call Romeo, and which we prove takes α-equivalent inputs to α-equivalent outputs. Then we use the same mechanics in PLT Redex to provide similar safety guarantees in that context, and demonstrate the ease of retrofitting existing Redex models to take advantage of our binding specifications.