BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mechanically verified LISP interpreters - Magnus Myreen (Universit
 y of Cambridge)
DTSTART:20081111T120000Z
DTEND:20081111T130000Z
UID:TALK13424@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:This talk describes work on constructing verified interpreters
  for a small LISP-like language using the interactive theorem prover HOL4.
  The LISP interpreters have been proved correct with respect to detailed x
 86\, ARM and PowerPC processor models. New techniques for expressing corre
 ctness of machine code were developed\, as well as new techniques for proo
 f-producing decompilation and compilation to/from HOL4 functions. A copyin
 g garbage collector (a Cheney collector) was verified and subsequent proof
 s were built upon its verified specification.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR