BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Characteristic Formulae for CakeML - Magnus Myreen\, Chal
 mers University
DTSTART:20170303T140000Z
DTEND:20170303T150000Z
UID:TALK71349@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Characteristic Formulae (CF) offer a productive\, principled a
 pproach to generating verification conditions for higher-order imperative 
 programs\, but so far the soundness of CF has only been considered with  r
 espect  to  an  informal  specification  of  a programming  language (OCam
 l). This leaves a gap between what is established by the verification fram
 ework and the program that actually runs. We present a fully-fledged CF fr
 amework for the formally specified CakeML programming language. Our framew
 ork extends the existing CF approach to support exceptions and I/O\, there
 by covering the full feature set of CakeML\, and comes with a formally ver
 ified soundness theorem. Furthermore\, it integrates  with  existing  proo
 f  techniques  for  verifying  CakeML  programs. This  validates  the  CF 
  approach\,  and  allows  users to  prove  end-to-end theorems for higher-
 order imperative programs\, from specification to language semantics\, wit
 hin a single theorem prover.
LOCATION:FW26
END:VEVENT
END:VCALENDAR