Speaker
Yuning Feng

Abstract
Realizability is about interpreting logical statements with programs. A statement is realizable if we can argue for it following some programs. In this talk, we discuss a variant of realizability on typed arithmetic: it has extensional equality, and to interprete an implication, a realizing program need to be total with respect to the antecedent's type. As a formal theory, much of this realizability is known using proof-theoretic methods, and the canonical model for it is well-known. However, it is still not clear what kind of category should this logic correspond to. Towards the problem, we propose a categorical construction with good properties. It is hoped that the categories obtained by the construction could serve as concrete solutions to the problem.