Join us for the FACS AGM followed by Peter Landin Semantics Seminar.
Speaker
Prof. David Pym, University College London
Agenda
4:00pm - FACS AGM
6:00pm - Peter Landin Semantics Seminar
Synopsis
FACS Annual General Meeting, followed by the annual FACS Peter Landin Semantics Seminar, delivered by by Prof. David Pym, University College London.
Inferentialism, Proof-theoretic Semantics, and Computation:
Peter Landin was one of instigators within the study of the semantics of programming languages of 'operational semantics’, the idea that language constructs derive meaning from the rules that govern their use. Peter explored these ideas through the reduction properties of lambda-terms, through the SECD machine, and through constructs such as the J-operator, which (like continuation semantics) hints at a connection between the operational and denotational. Much of my research lies within a field called ‘proof-theoretic semantics’. In this view of the foundations of logic, model-theoretic truth is replaced by proof-theoretic validity, and much of the essential foundational theory of logic can be reconstructed. I will explain how this works, some connections to computation, and a possible (proof-theoretic semantic) account of information. I think Peter would have approved of it all.
About the speaker
I am a logician, mathematician, and informatician.
My research is mainly in logic, where I work in pure logic, including - proof-theoretic semantics, also known as the theory of meaning, and its inferentialist philosophical context - the proof theory and semantics of reductive logic and proof-search (see, for example, Reductive Logic: Proof Theory, Semantics, and Control, by David Pym and Eike Ritter, Oxford Logic Guides, and the EPSRC-funded project ReLiC; reductive logic can be seen to be the foundation of automated reasoning, logic-based AI, and logic programming, including inductive logic programming, and - the semantics, proof theory, and applications of bunched logics.
I also work on developing logic-based methods as a mathematical modelling technology for reasoning about systems, security, and behaviour (see, for example, the EPSRC-funded project IRIS).
I am particularly interested in the philosophy and methodology of modelling. I am beginning to develop logic-based approaches to a semantic theory of information (in the philosophical spirit of situation theory) from the inferentialist perspective of proof-theoretic semantics.
Related to this is a developing interest in ideas from truthmaker semantics and possibility semantics.
I also work in information security, where I work in - the philosophy and methodology of security - security economics and policy, and - systems security modelling, with a focus on individual, organizational, and societal security behaviours. Together with my colleague Prof. Tyler Moore, I am Editor-in-Chief of OUP's Journal of Cybersecurity.
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 socio-economic-technical 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 proof-search, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of Cut-reduction; 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; utility-theoretic 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.
Our events are for adults aged 16 years and over.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.
This event is brought to you by: FACS (Formal Aspects of Computing Science) group
