BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Towards parametric direcursion: structured mixed-variant recursion
  with parameters - Johan Glimming (Visiting Research Fellow\, University o
 f Cambridge)
DTSTART:20090518T114500Z
DTEND:20090518T130000Z
UID:TALK18506@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:I will speak about Freyd's universal property generalising tha
 t of initial algebras and final coalgebras. This property\, termed direcur
 sion\, appears to be useful in programming language semantics. For example
 \, typical models of untyped lambda calculus and of object-based programmi
 ng languages come equipped with this property. Recent work on higher-order
  store have used recursive domain equations giving rise to the same proper
 ty. We here begin to develop a new reasoning principle with an aim to allo
 w both constant and modifiable (accumulating) parameters. In the case of i
 nitial algebras\, it is known (at least) since work by Cockett et al that 
 strong functors\, i.e. functors equipped with a natural transformation dis
 tributing a product over the endofunctor\, give rise to a parametric versi
 on of iteration in a cartesian closed category. We therefore ask how the s
 ituation generalises to mixed-variant bifunctors and direcursion\, and wha
 t universal property arises in this more general circumstance. It turns ou
 t that we require a generalisation of strength\, called distrength\, in ad
 dition to monoidal closed structure. Existence and uniqueness of solutions
  are demonstrated for the scheme\, under these assumptions\, by asymmetric
 ally reducing the scheme back to Freyd's work using the unit/counit of the
  assumed adjunction. Current work will be mentioned\, including the endeav
 our to express normalisation-by-evaluation by means of this generalised re
 cursion scheme (parametric direcursion).
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR