Structural Recursion With Locally Scoped Names
Locally scoped names are an important feature of the informal meta-theory of binding operations in programming languages and logics. Nominal sets provide a fruitful mathematical model of name scoping in the presence of recursive definitions. Previous work on formal languages based on this model (Pitts & Gabbay, 2000; Schopp & Stark, 2004; Cheney, 2009) uses some form of freshness information built into a type system in order to ensure that an expression using a locally scoped name, when interpreted in nominal sets, does not have the name in its support. In this paper, such 'Static freshness inference' is avoided by using an Odersky-style local scoping construct, which is given a new interpretation using nominal-sets-with-restriction, rather than just nominal sets.