Display Calculus for Bunched Logic

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

• James Brotherston, Imperial College London
• Friday 24 September 2010, 14:00-15:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

Display calculi, as formulated by Belnap in the 1980s, can be seen as natural successors of Gentzen’s sequent calculi, suitable for the proof-theoretic analysis of substructural and modal logics. They are characterised by the display property, which essentially states that proof judgments may be rearranged so that any chosen part appears alone on one side of the proof turnstile. Despite their theoretical elegance, display calculi seem to have been somewhat overlooked by the computer science community in the past.

Bunched logics, which originate in O’Hearn and Pym’s BI, are essentially free combinations of either classical or intuitionistic propositional logic with either classical or intuitionistic multiplicative linear logic. The practical interest in bunched logics stems from their resource interpretation, which underpins separation and spatial logics employed in program analysis. However, proof theory is something of a lacuna in this area: well-behaved proof systems for most variants of bunched logic have hitherto proven very difficult to find.

In this talk, we apply display calculus techniques to obtain a unified proof theory for all the principal varieties of bunched logic, and incidentally provide an explanation as to why well-behaved sequent calculi seem very unlikely to exist for most of these varieties.

This talk is based upon a related paper by the speaker:

James Brotherston. A unified display proof theory for bunched logic. In Proceedings of MFPS 2010 . Available from http://www.doc.ic.ac.uk/~jbrother/

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.