[TYPES/announce] World Logic Day at Swansea University on 14th January 2026: 3 talks: Arnold Beckmann, Ulrich Berger and John Tucker

[Monika Seisenberger]

Dear Colleagues and Friends,

On 14th January is World Logic Day!

Swansea University will contribute to World Logic Day with a hybrid event which will celebrate the significance and elegance of logic.
It is organised by the distinguished Theory Group at Swansea University<https://urldefense.com/v3/__https://www.swansea.ac.uk/compsci/research-and-impact/theoretical-computer-science/__;!!IBzWLUs!SNSIWo1liREH0q9E86QVhoF4YxwT_K1sHmSDThshWTDT-lVYiqZTR8o4kM74sVB0-I9QQw5ihuDv8dydcEc5QYpkc_kJm3tYA9hdDMnEx0Xn$ >, a leading centre for research in theoretical computer science,
and held under the auspices of the Robert Recorde Centre for Fundamental Studies, which is committed to advancing foundational research in mathematics, logic, and computer science.

Event page:  https://urldefense.com/v3/__https://sites.google.com/view/swanseaworldlogicday2026/__;!!IBzWLUs!SNSIWo1liREH0q9E86QVhoF4YxwT_K1sHmSDThshWTDT-lVYiqZTR8o4kM74sVB0-I9QQw5ihuDv8dydcEc5QYpkc_kJm3tYA9hdDIXzCR9v$ 

World Logic Day at Swansea Programme:

13:00 (GMT) Arnold Beckmann: Provably Total NP Search Problems of Bounded Arithmetic and beyond
Abstract: Total NP search problems are studied to characterise the complexity of natural search problems which cannot be analysed as decision problems.  Total NP search problems are clustered based on the reasoning used to prove that the search problem is total.  For provably total NP search problems, totality is guaranteed by a mathematical theory, in particular Bounded Arithmetic.
Bounded Arithmetic forms a collection of weak theories of Arithmetic related to complexity classes of functions like the Polynomial Time Hierarchy.  Many connections between Bounded Arithmetic and important questions about complexity classes have been established, including in form or provably total NP search problems.
In my talk, I will review the research programme of characterising provably total NP search problems in Bounded Arithmetic, and explain why it is important for current research in the area.  I will highlight recent results and point to future directions.

14:00 (GMT) Ulrich Berger: Non-strictly Positive Induction for Extracting Breadth-first Search
Abstract: In this talk I discuss a program that uses - somewhat surprisingly - a non-strictly positive inductive type to perform breadth-first search in a tree. The program goes back to Martin Hofmann ('Non strictly positive datatypes in system F', http://www.seas.upenn.edu/~sweirich/types/archive/1993/ ) and has been analysed from a type-theoretic and logical perspective (Ralph Matthes, Anton Setzer, B: "Martin Hofmann’s case for non-strictly positive data types", TYPES 2018 post-proceedings, LIPIcs 130).  The program will be used as an example for the use of general induction and coinduction principles for the extraction of provably correct programs.

15:00 (GMT0  John Tucker:  The History of Computability Theory and its Impact
Abstract: The history of computability theory is rich in deep concepts, and surprising theorems, applications and generalisations.  I will describe and reflect on some of its mathematical and philosophical achievements, including its roles in algebra and in theories of data, computing and AI, and on its social history.

Each talk will be 45 mins, including questions. Please feel free to join for one or for all talks. After each talk we can enjoy a coffee together.

Link to further World Logic Day 2026 events:
https://urldefense.com/v3/__https://wld.cipsh.international/wld2026.html__;!!IBzWLUs!SNSIWo1liREH0q9E86QVhoF4YxwT_K1sHmSDThshWTDT-lVYiqZTR8o4kM74sVB0-I9QQw5ihuDv8dydcEc5QYpkc_kJm3tYA9hdDPzj-WNw$ 

All welcome, Jay Morgan and Monika Seisenberger

--
Dr Monika Seisenberger
Associate Professor in Computer Science
Swansea University





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20260111/fc9707ab/attachment.htm>