Classical realizability as a classifier for nondeterminism

Guillaume Geoffroy

We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More s…