Basics and Contacts
Prof. David J. Pym, PhD (Edin), MA, ScD (Cantab), CMath FIMA, CITP FBCS
Professor of Information, Logic, and Security at UCL, University of London
Head of Programming Principles, Logic, and Verification (PPLV)
Turing Fellow, The Alan Turing Institute
University College London
Department of Computer Science
Gower Street
London WC1E 6BT
d.pym (at) ucl.ac.uk
Professor of Information, Logic, and Security at UCL, University of London
Head of Programming Principles, Logic, and Verification (PPLV)
Turing Fellow, The Alan Turing Institute
University College London
Department of Computer Science
Gower Street
London WC1E 6BT
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
My contributions have been mainly in the following areas: dependent type theory and logical frameworks, including proof theory, semantics, and unification algorithms; reductive logic and proofsearch, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of 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; utilitytheoretic 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.
I have broad experience of research, teaching, and management in leading universities and in industry.
Trust me, I'm a logician.
David's UCL CS Page
Short CV
  the proof theory and semantics of bunched logics,
  prooftheoretic semantics, 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 EPSRCfunded project ReLiC )
My contributions have been mainly in the following areas: dependent type theory and logical frameworks, including proof theory, semantics, and unification algorithms; reductive logic and proofsearch, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of 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; utilitytheoretic 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.
I have broad experience of research, teaching, and management in leading universities and in industry.
Trust me, I'm a logician.
David's UCL CS Page
Short CV
 Research Interests
 Recent and Selected Publications:
 Current drafts (html version)
 Logic and Systems Modelling (html version)
 Security and Policy (html version)
 Tools
 Older Publications
 Books (html version)
 Research Grants
 Alan Turing Institute
 UCL PPLV
 UCL Information Security
 Teaching
 UCL Roles
 Editorial Roles
 Short CV