BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:An Industrially Useful Prover - J Strother Moore (University of Te
 xas at Austin\; University of Edinburgh)
DTSTART:20170707T123000Z
DTEND:20170707T133000Z
UID:TALK73187@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:The ACL2 theorem prover is an interactive&nbsp\; automatic pro
 ver for the programming language<br>Common&nbsp\; Lisp.&nbsp\; It provides
  a convenient language for<br>building&nbsp\; prototypes of hardware and<b
 r>software designs\,&nbsp\; algorithms\, and other<br>computing systems.&n
 bsp\; In fact\, the&nbsp\; language is executed efficiently enough to<br>p
 ermit some&nbsp\; practical systems to be<br>built in it.&nbsp\; But ACL2 
 also&nbsp\; provides an environment for proving theorems<br>about&nbsp\; t
 hose prototypes.&nbsp\; In this talk I will demonstrate how<br><br>&nbsp\;
 ACL2 presents<br>itself to the user\, show a small example&nbsp\;<br>proof
  project about low-level code\, and discuss the&nbsp\; aspects of ACL2 tha
 t have made it attractive<br>as a tool&nbsp\; for industry.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR