Archive for the 'Locally named' Category

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.


External and internal syntax of the lambda-calculus

Masahiko Sato, from SCSS 2009, available from Masahiko Sato’s webpage:

It is well known that defining the substitution operation on λ-terms appropriately and establish basic properties like the substitution lemma is a subtle task if we wish to do it formally. The main obstacle here comes from the fact that unsolicited capture of free variables may occur during the substitution if one defines the operation naively.

We argue that although there are several approaches to cope with this problem, they are all unsatisfactory since each of them defines the λ- terms in terms of a single fixed syntax. We propose a new way of defining λ-terms which uses an external syntax to be used mainly by humans and an internal syntax which is used to implement λ-terms on computers.

In this setting, we will show that we can define λ-terms and the substitution operation naturally and can establish basic properties of terms easily.

Slides from a talk covering related work with Randy Pollack, presented at TAASN 2009, are available from Randy Pollack’s website.