Nominal System T

By Andrew Pitts, from POPL 2010, available from Andrew Pitts’ website:

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.

0 Responses to “Nominal System T”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: