Andrej Bauer: Parameterized realizability
Channel: FMF Foundations seminar
Date: 18/01/2024

Seminar for foundations of mathematics and theoretical computer science
Faculty of mathematics and physics
University of Ljubljana
January 18, 2024

Abstract: Parameterized partial combinatory algebras (ppca) are like ordinary partial combinatory algebras in which application receives an additional parameter from a fixed parameter set. The motivating example is the first Kleene algebra parameterized by a chosen set of oracles: the realizers are (codes of) oracle Turing machines and the parameters the oracles. A ppca is combinatory complete. Given a ppca, we may define a tripos whose consequence relation requires that realizers compute uniformly in the parameter set. The tripos begets a parameterized realizability topos which is similar to ordinary realizability toposes in some respects, but quite different in others. (See https://www.fmf.uni-lj.si/en/news/event/1343/andrej-bauer-parametric-realizability/)