- Supervisors: David Pym (UCL CS and Philosophy), Elaine Pimentel (UCL CS), Tim Button (UCL Philosophy) - Research group: Programming Principles, Logic, and Verification (PPLV)

- Project website: ucl-epsrc-dtp.github.io/2024-25-project-catalogue/projects/2228cd1286.html

- Application deadline: 13:00 UK time (GMT) on 08 January 2024

- Application website: www.ucl.ac.uk/epsrc-doctoral-training/prospective-students/apply-ucl-epsrc-dtp-studentship

- Supervisors' contact details (please use for informal discussions of the position):

• Pym: d.pym@ucl.ac.uk, www.cantab.net/users/david.pym/
• Pimentel: e.pimentel@ucl.ac.uk, sites.google.com/site/elainepimentel/home
• Button: tim.button@ucl.ac.uk, www.nottub.com

- Project Summary: Proof-theoretic semantics (P-tS) offers a practical foundation for the meaning of logical theories that is grounded inference — that is, reasoning — rather than the abstract structures of model theory. It lies within the philosophical position known as inferentialism. As such, P-tS offers an alternative foundation for mathematical logic that places reasoning at the heart of meaning.
    Non-classical, including substructural, logics are important classes of logics that support more controlled reasoning than classical logic. They have found significant academic and industrial application as the basis for tools for reasoning about program and system correctness, where their ability to support reasoning about the decomposition of structure is crucial in managing complexity and scale, and in AI. The treatment of substructural and other non-classical logics in P-tS, especially those of significance for agency, resource modelling, and theories of information (e.g., relevance/modal/epistemic logics), requires development.
    P-tS has two primary variants: Dummett-Prawitz validity, closely related to Brouwer-Heyting-Kolmogorov semantics, and base-extension semantics, which can be seen as bridge to model-theoretic semantics. Base-extension semantics will be the primary focus of this project, with the Dummett-Prawitz view also relevant.
   This studentship (intersecting informatics, mathematics, philosophy) will address giving proof-theoretic semantics to non-classical logics, developing the necessary abstract mathematical meta-theory and exploring the significance of inferentialist semantics, and its mathematical realization, for systems verification. This latter aspect will build directly on connections between the proof-theoretic foundations of logic programming and base-extension semantics recently established at UCL. Connections to simulation modelling and its inferentialist interpretation may be explored.
   The student will work with Prof. David Pym (Computer Science and Philosophy), Dr. Elaine Pimentel (Computer Science), and Prof. Tim Button (Philosophy), and be based in the Programming Principles, Logic, and Verification group.
   Candidates should have a Master’s degree in mathematics, philosophy, or computer science and a strong interest in logic.