[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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@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
