BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A verified runtime for a verified theorem prover - Magnus Myreen (
 University of Cambridge)
DTSTART:20110517T120000Z
DTEND:20110517T130000Z
UID:TALK31069@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION: Theorem provers\, such as ACL2\, HOL\, Isabelle and Coq\, rel
 y on the\n correctness of runtime systems for programming languages like M
 L\,\n OCaml or Common Lisp. Runtime systems are complex and critical to\n 
 the integrity of the theorem provers.\n\n In this paper\, we present a new
  Lisp runtime which has been designed\n to be trustworthy\, has been forma
 lly verified and can run the Milawa\n theorem prover. Our runtime\, which 
 consists of 7\,000 lines of\n machine code\, is able to complete a 4 gigab
 yte Milawa proof effort.\n\n The runtime includes a just-in-time compiler\
 , a copying garbage\n collector\, a parser and a printer\, all of which ar
 e HOL4-verified\n down to the concrete x86 code.  We make heavy use of our
  previously\n developed tools for machine-code verification. This work\n d
 emonstrates that our approach to machine-code verification scales\n to non
 -trivial applications.\n\nThis talk describes joint work with Jared Davis.
 \n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR