BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Culture clash: logic meets the real world - Nik Sultana (Universit
 y of Cambridge)
DTSTART:20151020T121500Z
DTEND:20151020T124500Z
UID:TALK61573@talks.cam.ac.uk
CONTACT:Heidi Howard
DESCRIPTION:Research on the automation of reasoning has made huge advances
  during recent decades. There is an increasing number of logic tools\, of 
 ever increasing strength\, and supporting an increasing number of applicat
 ions.\n\nBut something is rotten in the state of logic tool implementation
 s. It's still highly nontrivial to move logical evidence (especially proof
 s) between tools. This restricts what we can do with these tools.\n\nNow a
 t this point you might be thinking\, "why's this relevant to NetOS?". Well
 \, everything's connected\, right? :) Despite occurring in logic tools\, t
 his problem's essence isn't a logic problem: it's essentially to do with s
 ystem integration.\n\nThe difficulty described above arises because logic 
 tools are just tools: they suffer from the same shortcomings of other soft
 ware. Particularly research tools. Their documentation is often stale\, th
 e tools' behaviour is badly specified\, and the information they emit is o
 ften not sufficiently detailed to reconstruct in other tools.\n\nI'll talk
  about an approach that makes the transfer of data across logic tools more
  robust in the presence of such setbacks. This relies on two ideas: compil
 er phases\, and a more principled form of "tag soups". Logic tools need sy
 stems thinking.
LOCATION:Computer Laboratory\, William Gates Building\, Room FW11
END:VEVENT
END:VCALENDAR