Structural Recursion with Pure Local Names

I will discuss a new recursion principle for inductive data modulo alpha-equivalence of bound names that makes use of Odersky-style, effect-free local names when recursing over bound names. It is inspired by the nominal sets notion of "alpha-structural recursion". The new approach provides a pure calculus of total functions that still adequately represents alpha-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. It arises from a new semantics of Odersky-style local names using nominal sets.