BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Generic pattern unification: a categorical approach - Ambroise Laf
 ont\, University of Cambridge
DTSTART:20221021T130000Z
DTEND:20221021T140000Z
UID:TALK184931@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:We provide a generic categorical setting for Miller's\npattern
  unification. The syntax with metavariables is generated by a\nfree monad 
 applied to finite coproducts of representable functors\; the\nmost general
  unifier is computed as a coequaliser in the Kleisli\ncategory restricted 
 to such coproducts. Our setting handles\nsimply-typed second-order syntax\
 , linear syntax\, or (intrinsic)\npolymorphic syntax such as system F.\n\n
 (joint work with Neel Krishnaswami)
LOCATION:SS03
END:VEVENT
END:VCALENDAR
