Structural Recursion with Pure Local Names

Andrew Pitts (University of Cambridge)

Info

Date	13th November 2009 (week 5, Michaelmas Term 2009)
Time	14:00
Place	Lecture Theatre B

Abstract

I will discuss a new recursion principle for inductive data modulo alpha-equivalence of bound names that makes use of Odersky-style, effect-free local names when recursing over bound names. It is inspired by the nominal sets notion of "alpha-structural recursion". The new approach provides a pure calculus of total functions that still adequately represents alpha-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. It arises from a new semantics of Odersky-style local names using nominal sets.