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.