BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Virtue of certified programming with decision procedures - Vladimi
 r Komendantsky (St Andrews)
DTSTART:20120525T100000Z
DTEND:20120525T110000Z
UID:TALK38345@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:In this moderately technical talk\, I will discuss explicit te
 rmination of\ncomputations certified in Coq\, and recall the importance of
  correct decision\nprocedures for constructive understanding of computatio
 nal problems. I will\nrefer to examples of first-order definable relations
  on finite-state\ntransition systems to show how logical analysis can unde
 rpin different degrees\nof type dependencies.\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR