BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
X-WR-TIMEZONE:Europe/Amsterdam
BEGIN:VTIMEZONE
TZID:Europe/Amsterdam
X-LIC-LOCATION:Europe/Amsterdam
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:/NewsandEvents/Archives/2023/newsitem/14664/15
 -December-2023-Coinduction-a-Categorical-tour-of-C
 omputation-Liam-Chung
DTSTAMP:20231212T102448
SUMMARY:Coinduction: a Categorical tour of Computa
 tion, Liam Chung
ATTENDEE;ROLE=Speaker:Liam Chung
DTSTART;TZID=Europe/Amsterdam:20231215T160000
DTEND;TZID=Europe/Amsterdam:20231215T183000
LOCATION:TBD
DESCRIPTION:Induction is well known as both an imp
 ortant method of definition as well as proof, but 
 it has some important blind spots. Inductive defin
 itions use constructors, that is, methods to make 
 new objects. Inductively constructed data must hav
 e an end, in the context of real programs. This ma
 kes it more difficult to use for modelling computa
 tion with (possibly) infinite data streams, or whe
 re program termination is not guaranteed.  In this
  talk we'll discuss coinduction, the dual notion t
 o induction. Where induction is formulated as rule
 s for creating new things, coinduction is formulat
 ed as rules for taking them apart. This gives it w
 ide utility in modeling computational states witho
 ut assuming we know what they look like, a so-call
 ed black box approach.  We'll also delve into the 
 basics of the mathematical concepts underpinning t
 his duality, namely the duality of algebras and co
 algebras. While these topics take heavy inspiratio
 n from category theory and universal algebra, no p
 rior significant knowledge of either will be assum
 ed.
X-ALT-DESC;FMTTYPE=text/html:\n  <p>Induction is w
 ell known as both an important method of definitio
 n as well as proof, but it has some important blin
 d spots. Inductive definitions use constructors, t
 hat is, methods to make new objects. Inductively c
 onstructed data must have an end, in the context o
 f real programs. This makes it more difficult to u
 se for modelling computation with (possibly) infin
 ite data streams, or where program termination is 
 not guaranteed.</p>\n  <p>In this talk we'll discu
 ss coinduction, the dual notion to induction. Wher
 e induction is formulated as rules for creating ne
 w things, coinduction is formulated as rules for t
 aking them apart. This gives it wide utility in mo
 deling computational states without assuming we kn
 ow what they look like, a so-called black box appr
 oach.</p>\n  <p>We'll also delve into the basics o
 f the mathematical concepts underpinning this dual
 ity, namely the duality of algebras and coalgebras
 . While these topics take heavy inspiration from c
 ategory theory and universal algebra, no prior sig
 nificant knowledge of either will be assumed.</p>\
 n
URL:/NewsandEvents/Archives/2023/newsitem/14664/15
 -December-2023-Coinduction-a-Categorical-tour-of-C
 omputation-Liam-Chung
CONTACT:Paulius Skaisgiris, Josef Doyle at coollog
 ic.uva at gmail.com
END:VEVENT
END:VCALENDAR