Sciweavers

POPL
2010
ACM

Nominal System T

14 years 1 months ago
Nominal System T
This paper introduces a new recursion principle for inductive data modulo -equivalence of bound names. It makes use of Oderskystyle local names when recursing over bound names. It is formulated in an extension of G?odel'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 normalizationby-evaluation argument that makes use of a new semantics of local names in Gabbay-Pitts nominal sets. Categories and Subject Descriptors D.3.1 [Prog...
Andrew M. Pitts
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Andrew M. Pitts
Comments (0)