School of Electronic Engineering and Computer Science

Seminar: Resource semantics: substructural logic as a modelling technology

5 June 2018

Time: 1:00 - 2:00pm
Venue: ITL top floor, Queen Mary, University of London

Title: Resource semantics: substructural logic as a modelling technology

Speaker: David Pym, UCL

Host: Nikos Tzevelekos and Andrew Lewis-Smith


The development of the logic of bunched implications, BI, together with its somewhat characteristic resource semantics, led to the formulation of Separation Logic, which forms the basis of the Infer program analyser deployed in Facebook's code production. This rather successful story sits within a broader, quite systematic logical context. I will review the (family of) logics, including process logics, that are supported by resource semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating their uses in a range of modelling applications, including access control, systems security, and workflow simulation.

Directions, if coming from outside QMUL

Queen Mary is on Mile End Road, with nearest tube stations being Stepney Green (closest one to the seminars) and Mile End. The seminars are in the Informatics Teaching Laboratory, floor 2. As the building has card access, it is best to inform us that you will be coming.