BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proving Equivalences Between Prolog Semantics in Coq - Jael E Krie
 ner\, University of Kent
DTSTART:20130906T150000Z
DTEND:20130906T160000Z
UID:TALK46924@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Basing program analyses on formal semantics has a long and suc
 cessful tradition in the logic programming paradigm. These analyses rely o
 n results about the relative correctness of mathematically sophisticated s
 emantics\, and authors of such analyses often invest considerable effort i
 nto establishing these results. The development of interactive theorem pro
 vers such as Coq and their recent successes both in the field of program v
 erification as well as in mathematics\, poses the question whether these t
 ools can be usefully deployed in logic programming. This paper presents fo
 rmalisations in Coq of several general results about the correctness of se
 mantics in different styles\; forward and backward\, top-down and bottom-u
 p. The results chosen are paradigmatic of the kind of correctness theorems
  that semantic analyses rely on and are therefore well-suited to explore t
 he possibilities afforded by the application of interactive theorem prover
 s to this task\, as well as the difficulties likely to be encountered in t
 he endeavour. It turns out that the advantages offered by moving to a func
 tional setting\, including the possibility to apply higher-order abstract 
 syntax\, are considerable.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR