kirancodes.me
To Proof Maintenance & Beyond!

Romeo: a system for more flexible binding-safe programming

Paul Stansifer, Mitchell Wand

Abstract

Current languages for safely manipulating values with names only support term languages with simple binding syntax. As a result, no tools exist to safely manipulate code written in those languages for which name problems are the most challenging. We address this problem with Romeo, a language that respects α-equivalence on its values, and which has access to a rich specification language for binding, inspired by attribute grammars. Our work has the complex-binding support of David Herman's λm, but is a full-fledged binding-safe language like Pure FreshML.

Related papers