BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A refinement of the state monad - Johannes Borgstrom (MSR Cambridg
 e)
DTSTART:20091123T124500Z
DTEND:20091123T140000Z
UID:TALK20702@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Behavioural type and effect systems regulate properties such a
 s\nadherence to object and communication protocols\, dynamic security poli
 cies\,\navoidance of race conditions\, and many others. Typically\, each s
 ystem is\nbased on some specific syntax of constraints\, and is checked wi
 th an ad\nhoc solver.\n\nInstead\, we advocate types refined with first-or
 der logic formulas as a\nbasis for behavioural type systems\, and general 
 purpose automated theorem\nprovers as an effective means of checking progr
 ams.\n\nTo illustrate this approach\, we give type systems for two related
  notions\nof permission-based access control: stack inspection and history
 -based access\ncontrol. These type systems are both instances of a refined
  state monad.\n\nOur main technical result is a safety theorem stating tha
 t no assertions\nfail when running a well-typed program.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR