BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proof-Producing Synthesis of ML from Higher-Order Logic - Magnus M
 yreen (University of Cambridge)
DTSTART:20120313T130000Z
DTEND:20120313T140000Z
UID:TALK35579@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:Theorem provers such as Coq\, Isabelle/HOL\, HOL4\, etc. provi
 de mechanisms that print (sometimes called extract) functions from the log
 ic into functions in real programming languages\, e.g. ML or Haskell.\n\nI
 n this talk I'll describe how this printing can be made into a trustworthy
  step. I'll show how the translation from logic into a programming languag
 e can be automatically performed via proof --- a proof which states that t
 he translation is semantics preserving with respect to the logic and an op
 erational semantics of the target language\, in our case a pure ML-like la
 nguage.\n\nThe technique described in this talk applies to recursive funct
 ions\, type variables\, functions as first-class objects\, user-defined da
 tatypes\, nested pattern matching and partiality\, e.g. arising from missi
 ng cases in pattern matching.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR