Structural Recursion with Locally Scoped Names (Abstract)
This paper introduces a new recursion principle for inductively
defined data modulo α-equivalence of bound names that makes
use of Odersky-style local names when recursing over bound names. It
is formulated in simply typed λ-calculus extended with names
that can be restricted to a lexical scope, tested for equality,
explicitly swapped and abstracted. The new recursion principle is
motivated by the nominal sets notion of "α-structural
recursion", whose use of names and associated freshness
side-conditions in recursive definitions formalizes common practice
with binders. The new calculus has a simple interpretation in
nominal sets equipped with name restriction operations. It is shown
to adequately represent α-structural recursion while avoiding
the need to verify freshness side-conditions in definitions and
computations. The paper is a revised and expanded version of [AM
Pitts, "Nominal System T", Proc. ACM POPL 2010].