[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Fully 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)
- Project website:
https://urldefense.com/v3/__https://ucl-epsrc-dtp.github.io/2024-25-project-catalogue/projects/2228cd1286.html__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x4pB_5sSQ$
- Application deadline: 13:00 UK time (GMT) on 08 January 2024
- Application website:
https://urldefense.com/v3/__https://www.ucl.ac.uk/epsrc-doctoral-training/prospective-students/apply-ucl-epsrc-dtp-studentship__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x5JqiWhLQ$
- Supervisors' contact details (please use for informal discussions of the
position):
Pym: [email protected],
https://urldefense.com/v3/__https://www.cantab.net/users/david.pym/__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x4kRJw1wg$
Pimentel: [email protected],
https://urldefense.com/v3/__https://sites.google.com/site/elainepimentel/home__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x5L3mA_vg$
Button: [email protected],
https://urldefense.com/v3/__https://www.nottub.com/__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x6yOQwBCQ$
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.
--
Prof. David J. Pym
Professor of Information, Logic, and Security
Department of Computer Science & Department of Philosophy
Head of Programming Principles, Logic, and Verification
University College London
Research Fellow and Director of the Centre for Logic and Language (CeLL)
Institute of Philosophy, University of London
Director, UCL Centre for Doctoral Training in Cybersecurity
Editor-in-Chief, OUP Journal of Cybersecurity
[email protected]
https://urldefense.com/v3/__http://www.cs.ucl.ac.uk/people/D.Pym.html__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x4v1Ctd7g$
https://urldefense.com/v3/__http://www.cs.ucl.ac.uk/staff/D.Pym/__;!!IBzWLUs!Ubex3UnxCXnY16lHS9GkcIFyaapCtjXBwRH_9xNZF1V52Nk5VsvaL_Q3GURy2toIfyqWG5WmzMqvlTAm6bno_x6K0Xjaeg$
Assistant: Julia Savage, [email protected], +44 (0)20 7679 0327
