A General Notion of Realizability
L. Birkedal
Abstract
We present a general notion of realizability encompassing both standard
Kleene style realizability over partial combinatory algebras and Kleene
style realizability over more general structures, including all partial
cartesian closed categories. We show how the general notion of
realizability can be used to get models of dependent predicate logic,
thus obtaining as a corollary (the known result) that the category
Equ of equilogical spaces models dependent predicate logic.
Moreover, we characterize when the general notion of realizability gives
rise to a topos.