Functional Programming Seminar: Structural Recursion with Pure Local Names

Location: C60 Computer Science Building
Date(s): Friday 19th February 2010 (16:00-17:00)
Description: Speaker: Andrew Pitts (University of Cambridge)

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.

see http://fp.cs.nott.ac.uk/index.php?option=com_content&view=article&id=55&Itemid=66

School of Computer Science

University of Nottingham
Jubilee Campus
Wollaton Road
Nottingham, NG8 1BB

For all enquires please visit:
www.nottingham.ac.uk/enquire