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
Department of Philosophy (Affiliated Faculty)
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)
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
Department of Philosophy (Affiliated Faculty)
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 informatician. My research is
mainly in logic, where I work in pure logic, including
I also work in information security, where I work in
While my main research interests lie in the foundations of logic, as described above, my overall perspective unifies these aspects of my work: I am interested in developing foundations, frameworks, theories, and tools for understanding and reasoning about the complex socioeconomictechnical 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 proofsearch, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of Cutreduction; 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.
  prooftheoretic semantics, also known as the theory of meaning,
  the proof theory and semantics of reductive logic and proofsearch (see, for example,
 Reductive Logic: Proof Theory, Semantics, and Control, by David Pym and Eike
 Ritter, Oxford Logic Guides, and the EPSRCfunded project ReLiC); reductive logic
 can be seen to be the foundation of automated reasoning, logicbased AI, and logic
 programming, including inductive logic programming, and
  the semantics, proof theory, and applications of bunched logics.
I also work in information security, where I work in
  the philosophy and methodology of security
  security economics and policy, and
  systems security modelling,
While my main research interests lie in the foundations of logic, as described above, my overall perspective unifies these aspects of my work: I am interested in developing foundations, frameworks, theories, and tools for understanding and reasoning about the complex socioeconomictechnical 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 proofsearch, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of Cutreduction; 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.
Information
David's UCL CS PageShort CV
 Recent and Selected Publications:
 Current Drafts and Recent Papers (html version)
 Logic and Systems Modelling (html version)
 Security and Policy (html version)
 Tools
 Older Publications
 Research Grants
 EU Marie SklodowskaCurie RISE Project: MOSAIC.
 EPSRC Programme Grant IRIS
 EPSRC Research Grant ReLiC
 Previous EPSRC research grants at Grants on the Web
 Previously funded by the UK's Technology Strategy Board, the EU, the Royal Society, and the British Council
 Institute of Philosophy
 UCL PPLV
 UCL Information Security
 Teaching
 UCL Roles
 Editorial Roles