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.

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.

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.