2013/09/03 by Santos, Walter Ferrer, Guillermo, Mauricio, Malherbe, Octavio
#FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.1309.0706
Besides recalling the basic definitions of Realizability Lattices, Abstract Krivine Structures, Ordered Combinatory Algebras and Tripos and reviewing its relationships, we propose a new foundational framework for realizability. Motivated by Streicher's paper "Krivine's Classical Realizability from a Categorical Perspective" [9], we define the concept of Krivine's Ordered Combinatory Algebras (kOKA) as a common platform that is strong enough to do both: categorical and computational semantics. The OCAs produced by Streicher from AKSs in [9] are particular cases of kOKAs.