Flexible binding-safe programming
Paul Stansifer · 2016
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.