BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automating proof by induction in Isabelle/HOL using domain-specifi
 c languages - Yutaka Nagashima\, Czech University in Prague (CTU) &amp\; U
 niversity of Innsbruck
DTSTART:20200304T100000Z
DTEND:20200304T102000Z
UID:TALK140371@talks.cam.ac.uk
CONTACT:Jean Pichon-Pharabod
DESCRIPTION:Isabelle/HOL offers the induction tactic to facilitate inducti
 ve proofs.  However\, it still requires human ingenuity to decide what arg
 uments to pass to the induction tactic.  To automate this process\, I deve
 loped two domain-specific languages\, PSL and LiFtEr.  PSL attempts to fin
 d out the right combination of arguments to the induction tactic through a
  search\, whereas LiFtEr identifies promising combinations of arguments wi
 thout relying on a search.  Our evaluation demonstrated that PSL and LiFtE
 r produce valuable recommendations across problem domains.
LOCATION:Computer Lab\, FW11
END:VEVENT
END:VCALENDAR