Structural recursion with pure local names

Add to your list(s) Download to your calendar using vCal

• Andy Pitts (University of Cambridge)
• Monday 09 November 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.