<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div><br>
</div>
<div>
<div><br>
</div>
<div>Fully funded PhD Studentship in Proof-theoretic Semantics at UCL </div>
<div><br>
</div>
<div>- Supervisors: David Pym (UCL CS and Philosophy), Elaine Pimentel (UCL CS), Tim Button </div>
<div> (UCL Philosophy)</div>
<div><br>
</div>
<div>- Research group: Programming Principles, Logic, and Verification (PPLV)</div>
<div><br>
</div>
<div>- Project website: https://ucl-epsrc-dtp.github.io/2024-25-project-catalogue/projects/2228cd1286.html</div>
<div><br>
</div>
<div>- Application deadline: 13:00 UK time (GMT) on 08 January 2024 </div>
<div><br>
</div>
<div>- Application website: https://www.ucl.ac.uk/epsrc-doctoral-training/prospective-students/apply-ucl-epsrc-dtp-studentship </div>
<div><br>
</div>
<div>- Supervisors' contact details (please use for informal discussions of the position): </div>
<div><br>
</div>
<div> Pym: d.pym@ucl.ac.uk, https://www.cantab.net/users/david.pym/</div>
<div> </div>
<div> Pimentel: e.pimentel@ucl.ac.uk, https://sites.google.com/site/elainepimentel/home</div>
<div> </div>
<div> Button: tim.button@ucl.ac.uk, https://www.nottub.com/ </div>
<div><br>
</div>
<div><br>
</div>
<div>Project Summary</div>
<div><br>
</div>
<div>Proof-theoretic semantics (P-tS) offers a practical foundation for the meaning </div>
<div>of logical theories that is grounded inference — that is, reasoning — rather </div>
<div>than the abstract structures of model theory. It lies within the philosophical </div>
<div>position known as inferentialism. As such, P-tS offers an alternative foundation </div>
<div>for mathematical logic that places reasoning at the heart of meaning.</div>
<div><br>
</div>
<div>Non-classical, including substructural, logics are important classes of logics </div>
<div>that support more controlled reasoning than classical logic. They have found </div>
<div>significant academic and industrial application as the basis for tools for </div>
<div>reasoning about program and system correctness, where their ability to support </div>
<div>reasoning about the decomposition of structure is crucial in managing complexity </div>
<div>and scale, and in AI. The treatment of substructural and other non-classical </div>
<div>logics in P-tS, especially those of significance for agency, resource modelling, </div>
<div>and theories of information (e.g., relevance/modal/epistemic logics), requires </div>
<div>development.</div>
<div><br>
</div>
<div>P-tS has two primary variants: Dummett-Prawitz validity, closely related to </div>
<div>Brouwer-Heyting-Kolmogorov semantics, and base-extension semantics, which can </div>
<div>be seen as bridge to model-theoretic semantics. Base-extension semantics will </div>
<div>be the primary focus of this project, with the Dummett-Prawitz view also relevant.</div>
<div><br>
</div>
<div>This studentship (intersecting informatics, mathematics, philosophy) will address </div>
<div>giving proof-theoretic semantics to non-classical logics, developing the necessary </div>
<div>abstract mathematical meta-theory and exploring the significance of inferentialist </div>
<div>semantics, and its mathematical realization, for systems verification. This latter </div>
<div>aspect will build directly on connections between the proof-theoretic foundations </div>
<div>of logic programming and base-extension semantics recently established at UCL. </div>
<div>Connections to simulation modelling and its inferentialist interpretation may be </div>
<div>explored.</div>
<div><br>
</div>
<div>The student will work with Prof. David Pym (Computer Science and Philosophy), </div>
<div>Dr. Elaine Pimentel (Computer Science), and Prof. Tim Button (Philosophy), </div>
<div>and be based in the Programming Principles, Logic, and Verification group.</div>
<div><br>
</div>
<div>Candidates should have a Master’s degree in mathematics, philosophy, or </div>
<div>computer science and a strong interest in logic.</div>
<div><br>
</div>
</div>
<br>
<div>
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div>--</div>
<div>Prof. David J. Pym <br>
Professor of Information, Logic, and Security <br>
Department of Computer Science & Department of Philosophy <br>
<br>
Head of Programming Principles, Logic, and Verification<br>
University College London<br>
<br>
Research Fellow and Director of the Centre for Logic and Language (CeLL)<br>
Institute of Philosophy, University of London<br>
<br>
Director, UCL Centre for Doctoral Training in Cybersecurity<br>
Editor-in-Chief, OUP Journal of Cybersecurity<br>
<br>
d.pym@ucl.ac.uk<br>
www.cs.ucl.ac.uk/people/D.Pym.html<br>
www.cs.ucl.ac.uk/staff/D.Pym/<br>
<br>
Assistant: Julia Savage, j.savage@ucl.ac.uk, +44 (0)20 7679 0327</div>
<div><br>
</div>
</div>
<br class="Apple-interchange-newline">
<br class="Apple-interchange-newline">
</div>
<br>
</body>
</html>