BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Core Quantitative Coeffect Calculus - Marco Gaboardi (University
  of Dundee)
DTSTART:20140505T100000Z
DTEND:20140505T110000Z
UID:TALK52239@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:Linear logic is well known for its resource-awareness\, which 
 has inspired the design of several resource management mechanisms in progr
 amming language design. Its resource-awareness arises from the distinction
  between linear\, single-use data and non-linear\, reusable data. The latt
 er is marked by the so-called exponential modality\, which\, from the cate
 gorical viewpoint\, is a (monoidal) comonad.\n\nMonadic notions of computa
 tion are well-established mechanisms used to express effects in pure funct
 ional languages. Less well-established is the notion of comonadic computat
 ion. However\, recent works have shown the usefulness of comonads to struc
 ture context dependent computations. In this talk\, I will present a langu
 age inspired by a generalized interpretation of the exponential modality. 
 In this language the exponential modality carries a label—an element of 
 a semiring—that provides additional information on how a program uses it
 s context. This additional structure is used to express comonadic type ana
 lysis\n\nI will conclude my talk by discussing an ongoing work about a qua
 ntitative calculus combining comonadic coeffects with monadic effects. I w
 ill show how a dependency between coeffects and effects corresponds to a d
 istributivity law of (labeled) monads over (labeled) comonads.
LOCATION:FW11
END:VEVENT
END:VCALENDAR