Realizability in OCAs and AKSs

Abstract

In the context of the $\mathcal{O}\mathcal{C}\mathcal{A}$ associated to an $\mathcal{A}\mathcal{K}\mathcal{S}$ we introduce a closure operator and two associated maps that replace the closure and the maps defined in \cite{kn:ocar}. We were motivated by the search of a full adjunction to the original implication map. We show that all the constructions from $\mathcal{O}\mathcal{C}\mathcal{A}$s to triposes developped in \cite{kn:ocar} can be also implemented in the new situation.

References in corpus (1)

• A Report on Realizability

Cited by in corpus (2)

• Classical and Relative Realizability
• Revisiting the duality of computation: an algebraic analysis of classical realizability models