Culture clash: logic meets the real world

Add to your list(s) Download to your calendar using vCal

• Nik Sultana (University of Cambridge)
• Tuesday 20 October 2015, 13:15-13:45
• Computer Laboratory, William Gates Building, Room FW11.

If you have a question about this talk, please contact Heidi Howard.

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 applications.

But something is rotten in the state of logic tool implementations. It’s still highly nontrivial to move logical evidence (especially proofs) between tools. This restricts what we can do with these tools.

Now at this point you might be thinking, “why’s this relevant to NetOS?”. Well, everything’s connected, right? :) Despite occurring in logic tools, this problem’s essence isn’t a logic problem: it’s essentially to do with system integration.

The difficulty described above arises because logic tools are just tools: they suffer from the same shortcomings of other software. Particularly research tools. Their documentation is often stale, the tools’ behaviour is badly specified, and the information they emit is often not sufficiently detailed to reconstruct in other tools.

I’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: compiler phases, and a more principled form of “tag soups”. Logic tools need systems thinking.

This talk is part of the Computer Laboratory NetOS Group Talklets series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory NetOS Group Talklets
• Computer Laboratory, William Gates Building, Room FW11
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.