BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Coeffect Systems and Typing (Preliminary report) - Tomas Petricek 
 &amp\; Dominic Orchard (Computer Laboratory\, Cambridg)
DTSTART:20111007T141500Z
DTEND:20111007T151500Z
UID:TALK33689@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:_Effect systems_ are a class of static program analyses tracki
 ng information about side effects in a program\, such as read/write effect
 s and exceptions. The traditional approach to describing effect systems is
  to augment the typing rules of a language with effect judgements.\n\nIn s
 emantics and functional programming\, _monads_ are popularly used as a mea
 ns of structuring side effecting computations. Both monads and effect syst
 ems can be combined into one uniform system\, where monadic types are "tag
 ged" with effect information (see _The Marriage of Monads and Effects_ by 
 Wadler and Thiemann). The standard operations of a monad\, providing compo
 sitional semantics\, are augmented so that effect information is composed\
 , matching the rules of an effect system.\n\nThis work considers the dual 
 situation\, of "coeffect" systems structured by comonads and comonadic-typ
 ing.\n\nNumerous type systems have been proposed to track how computations
  depend on the "context" of execution. A context-dependent computation may
  only execute in certain environments or in a sandbox that provides suffic
 ient privileges. We term such context-dependence _coeffects_. \n\nIn this 
 talk\, we show how to track different kinds of context-dependence in a uni
 form way using a type system based on _comonads_.\n\nThis is a talk on pre
 liminary results and ideas\, and is by no means polished.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR