BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:TALK CANCELLED: An overview of structural corecursion - Venanzio C
 apretta (University of Nottingham)
DTSTART:20090424T130000Z
DTEND:20090424T140000Z
UID:TALK17295@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:The topic of the talk is programming over infinite structures.
  Non-wellfounded objects can be represented and manipulated by recursive f
 unctions whose circularity is restricted in several ways. We do not yet ha
 ve a satisfactory theory of what recursive definitions should be allowed a
 nd how we can reason over them. I will give an overview of the main questi
 ons that we are facing and then describe an approach to an abstract charac
 terisation of corecursion that we are developing.\n\nThe notion of corecur
 sive algebra characterises structures whose elements contain infinite info
 rmation. Functions into them can be defined by infinite iteration of produ
 ctive procedures.\n\nOn the other hand\, the notion of antifounded algebra
  characterises structures on which we can reason by using bisimulation. It
  is not a surprise that this concept is more general than that of corecurs
 ive algebra: the principle of bisimulation holds also for wellfounded stru
 ctures\, although it is equivalent with the more manageable structural equ
 ality.\n\nThe real surprise of our research is that not all corecursive al
 gebras are antifounded. We found a structure that satisfies the principle 
 of corecursion but not that of bisimulation. It is constructed by exploiti
 ng a certain colouring of the edges of an infinite tree.\n\nI will introdu
 ce and illustrate the notion and then describe our counterexample.\n\nWork
  in collaboration with Tarmo Uustalu and Varmo Vene.\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR