Nominal System T (Abstract)
This paper introduces a new recursion principle for inductive data
modulo α-equivalence of bound names. It makes use of
Odersky-style local names when recursing over bound names. It is
formulated in an extension of Gödel's System T with names that can
be tested for equality, explicitly swapped in expressions and
restricted to a lexical scope. 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 Nominal System T presented here
provides a calculus of total functions that is shown to adequately
represent α-structural recursion while avoiding the need to
verify freshness side-conditions in definitions and
computations. Adequacy is proved via a normalization-by-evaluation
argument that makes use of a new semantics of local names in
Gabbay-Pitts nominal sets.