Websites:
https://www.cantab.net/users/david.pym/ and
http://www.cs.ucl.ac.uk/staff/D.Pym/
Basics and Contacts:
Prof. David J. Pym, PhD (Edin), MA, ScD (Cantab), CMath FIMA, CITP FBCS, FRSA
Professor of Information, Logic, and Security at UCL, University of London
Head of Programming Principles, Logic, and Verification (PPLV)
Honorary Research Fellow, Institute of Philosophy, School of Advanced Study, University of London
Director of UCL's Centre for Doctoral Training in Cybersecurity
University College London,
Department of Computer Science and
Department of Philosophy,
Gower Street,
London WC1E 6BT.
Email: d.pym (at) ucl.ac.uk
Assistant: Julia Savage
Email: j.savage (at) ucl.ac.uk; telephone: +44 (0)20 7679 0327 (direct); 30327 (internal)
Brief Bio and Short CV:
I am a logician, mathematician, and computer scientist. My research is mainly in logic, where I work in pure logic, including
- the semantics, proof theory, and applications of bunched logics,
- proof-theoretic semantics, also known as the theory of meaning, and
- the proof theory and semantics of reductive logic (see, for example, Reductive Logic:
Proof Theory, Semantics, and Control, by David Pym and Eike Ritter,
Oxford Logic Guides and the EPSRC-funded project ReLiC); reductive logic can be
seen to be the foundation of automated reasoning, logic-based AI, and
logic programming, including inductive logic programming.
I also work on developing logic-based methods as a mathematical modelling technology for reasoning about systems, security, and behaviour (see, for example, the EPSRC-funded project IRIS). I am beginning to develop logic-based approaches to a semantic theory of information (in the philosophical spirit of situation theory). Related to this a developing interest in truthmaker semantics.
I also work in information security, where I work in
- security policy,
- security economics, and
- systems security modelling,
with a focus on individual, organizational, and societal security behaviours. I am Editor-in-Chief of OUP's Journal of Cybersecurity.
My overall perspective unifies these aspects of my work: I am interested in developing frameworks, theories, and tools for understanding and reasoning about the complex socio-economic-technical systems that define and support our world.
My contributions have been mainly in the following areas: dependent type theory and logical frameworks, including proof theory, semantics, and a unification algorithm; reductive logic and proof-search, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of Cut-reduction; the bunched logic BI and its relatives, including proof theory, semantics, algebraic theory, and computational interpretations, and their applications to program logics, including Separation Logic, and security; distributed systems modelling based on resource semantics and process algebra; modal and epistemic bunched logics and layered graph logics, with applications in access control; utility-theoretic concepts in distributed systems modelling and process algebra, with applications in systems security modelling; trust domains; information security economics; the philosophy and methodology of information security; public policy in information security, including information stewardship.
