Andrej Bauer: Parametric realizability

Date of publication: 16. 1. 2024
Mathematics and theoretical computing seminar
10:00 - 12:00
Jadranska 21, 3.07

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.