BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Machine Learning for Interactive Theorem Proving: Revisit\, Reuse 
 and Recycle your Proofs - Katya Komendenskaya (Heriot-Watt University)
DTSTART:20170713T150000Z
DTEND:20170713T160000Z
UID:TALK73274@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Interactive theorem proving has seen major development in the 
 past decade\, &nbsp\;and is being &nbsp\;widely adopted in&nbsp\;formalisa
 tion of mathematics and in verification. Further growth and dissemination 
 of interactive theorem proving &nbsp\;require more intelligent tools that 
 can make this technology more user friendly and convenient.&nbsp\;As full 
 automation of interactive provers is impossible\, it is important to&nbsp\
 ;develop better heuristics that enableto data mine the existing libraries 
 and &nbsp\;reuse existing proof strategies when writing new proofs.In this
  talk\, I will talk about several projects devoted to Machine Learning for
  Interactive Theorem Proving (in Coq and ACL2)&nbsp\; that I participated 
 in in&nbsp\;the last 5 years.I will give a light survey of a variety of ma
 chine learning methods that have already been employed in these&nbsp\;prov
 ers\, and will discuss\, with some help from the audience\, which of those
  methods bear more promise for the future.&nbsp\;In the technical part\, I
  will also talk about ML4PG --&nbsp\;&nbsp\;the machine learning extension
  to Proof general\, that I have developed in collaboration with &nbsp\;my 
 colleagues\, its recent extension Coq-PR3&nbsp\;and the plans to re-incarn
 ate these tools&nbsp\;in the upcoming new version of Proof General current
 ly developed by INRIA and at MIT.&nbsp\;&nbsp\;&nbsp\;&nbsp\;Based on the 
 joint work with G.Grov\, &nbsp\;T.Gransden\,&nbsp\;&nbsp\;J.Heras\, M.Joha
 nsson\, E.McLean\, N.Walkinshaw.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR