BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Halo: From Haskell to Logic through Denotational Semantics - Dimit
 rios Vytiniotis\, MSR Cambridge
DTSTART:20121123T140000Z
DTEND:20121123T150000Z
UID:TALK41163@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:Even well-typed programs can go wrong\, by encountering a patt
 ern-match failure\, or simply returning the wrong answer. And increasingly
 -popular response is to allow programmers to write contracts that express 
 behavioural properties\, such as crash-freedome of some useful post-condit
 ion. We study the static verification of such contracts. Our main contribu
 tion is a novel translation to first-order logic of both Haskell programs\
 , and contracts written in Haskell\, all justified by denotational semanti
 cs. This translation enables us to prove that functions satisfy their cont
 racts using off-the-shelf first-order theorem provers.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR