Professor David J. Pym
6th Century Chair in Logic, and SICSA Professor of Computing Science
University of Aberdeen

School of Natural and Computing Sciences
University of Aberdeen
King's College
Aberdeen AB24 3UE
Scotland, U.K.

Room: 059 Meston
Email: David Pym
Telephone: +44 (0)1 224 27 4577
Fax: +44 (0)1 224 27 2943

New University of Aberdeen Master's programme in Cloud Computing.

Please consider submitting to, and attending, WEIS 2012.

• Recent Publications

I am one of the designers of the Core Gnosis tool for systems and security modelling. The Core Gnosis system can be downloaded from HP Labs at http://www.hpl.hp.com/research/systems_security/gnosis.html, along with a paper

M. Collinson, B. Monahan, and D. Pym,
Semantics for Structured Systems Modelling and Simulation,
Proc. Simutools 2010, ACM Digital Library and EU Digital Library, ISBN: 978-963-9799-87-5,

published at SIMUTools 2010.

Research Interests

I am currently interested in, and interested in supervising PhD students in, the following areas:

• Mathematical systems modelling, using algebraic, logical, and stochastic methods, with applications in information security;
• Topics related to the economics of information security;
• Topics related to the economics of systems thinking;
• Topics connecting logic (substructural, modal; process algebra) and utility theory;
• Topics in logic related to information flow and trust domains;
• Topics related to information security, information stewardship, and cloud computing;
• Topics in logic related to the theory of search spaces.

Current Funded Projects

• Trust Economics (TSB Funding, Project Manager and scientific leader, consultant to HP Labs). This project takes a whole-systems view of information security, including economic, human, and technologicial issues. Partners in the project are HP Labs, the Universities of Bath and Newcastle, and UCL. National Grid is closely associated with the project.
• Cloud Stewardship Economics: Securing the New Business Infrastructure (TSB funding, scientific leader, consultant to HP Labs). This project is concerned with economics of cloud computing. In particular, it is concerned with the economics of information stewardship in cloud computing ecosystems. Partners in the project are HP Labs (lead site; Simon Shiu, Project Manager), the University of Aberdeen's Business School, the University of Bath, Validsoft, Sapphire, and Marmalade Box.
• Trust Domains (TSB and RCUK Digital Economy Programme funding). Our partners are HP Labs, Bristol (lead site; Dirk Kuhlmann, Project Manager), Perpetuity Group, University of Birmingham, and University of Oxford. 3 years from 1 April, 2011.
• Coming soon: SECONOMICS (EU FP7 funding; with Julian Williams, Fabio Massacci, Robert Coles, and others). Socio-economic aspects of security policy. Various European partners including National Grid.

Recent Funded Projects (see Recent Publications for associated papers)

• The Semantics of Classical Proofs (EPSRC funding, with Martin Hyland and Edmund Robinson). This project developed categorical models for the (propositional) classical sequent calculus, establishing soundness and completeness results, and making connections with proof nets, the Geometry of Interaction, and related ideas. Richard McKinley's (Bath) PhD thesis (supervised by Pym and Führmann) extended the ideas to classical predicate logic and made some connections with the calculus of structures and classical model theory.
• Bunched ML (EPSRC funding, with Peter O'Hearn and Edmund Robinson). This project developed type systems and categorical models for ML-like languages with type systems using the substructural constructs of bunched logic. Compared to languages using the usual ML-like type systems, such languages have cleaner treatments of concepts in memory management such as locations, regions, allocation, and disposal.

Monographs

• A Discipline of Mathematical Systems Modelling, joint work with Matthew Collinson and Brian Monahan, to be published by the open-access publisher College Publications.
• Reductive Logic and Proof-search: Proof Theory, Semantics, and Control, joint work with Eike Ritter, published by Oxford University Press in its Oxford Logic Guides series. Here is the page for its Errata and Remarks.
• The Semantics and Proof Theory of the Logic of Bunched Implications, together with its Errata and Remarks (also here), published by Springer. Here is the home page for BI, the Logic of Bunched Implications. Here is a link to a movie about BI.