You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Matteo Capucci (he/him) (Oct 30 2023 at 09:15):From #general: mailing list mirror:
From: Pym, David <d.pym@ucl.ac.uk>
Sent: Friday, October 27, 2023 10:05 PM
To: Categories mailing list <categories@mq.edu.au>
Subject: Fully funded PhD Studentship in Proof-theoretic Semantics at UCLFully funded PhD Studentship in Proof-theoretic Semantics at UCL
Supervisors: David Pym (UCL CS and Philosophy), Elaine Pimentel (UCL CS), Tim Button
(UCL Philosophy)Research group: Programming Principles, Logic, and Verification (PPLV)
Application deadline: 13:00 UK time (GMT) on 08 January 2024
Application website: https://www.ucl.ac.uk/epsrc-doctoral-training/prospective-students/apply-ucl-epsrc-dtp-studentship<https://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, https://www.cantab.net/users/david.pym/<https://www.cantab.net/users/david.pym/>
Pimentel: e.pimentel@ucl.ac.uk, https://sites.google.com/site/elainepimentel/home<https://sites.google.com/site/elainepimentel/home>
Button: tim.button@ucl.ac.uk, https://www.nottub.com/<https://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.