LOGIKSEMINARIET STOCKHOLM-UPPSALA

On Wednesday November 10

Andrew Pitts (Cambridge) gives a seminar with the title

 	Structural Recursion with Locally Scoped Names

at 10.30 - 12.15 in room 1213, building 1, MIC, Polacksbacken, Uppsala

Abstract:

I will discuss a new recursion principle for inductive data modulo
alpha-equivalence of bound names that makes use of Odersky-style 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.


----

Andrew Pitts is Professor of Theoretical Computer Science at the University of 
Cambridge.

www.cl.cam.ac.uk/users/amp12