Classical and Relative Realizability

Jaap van Oosten, Tingxiang Zou

We show that every abstract Krivine structure in the sense of Streicher can be obtained, up to equivalence of the resulting tripos, from a filtered opca (A,A') and a subobject of 1…