A Report on Realizability
Logic
2013-10-01 v3
Abstract
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.
Keywords
Cite
@article{arxiv.1309.0706,
title = {A Report on Realizability},
author = {Walter Ferrer Santos and Mauricio Guillermo and Octavio Malherbe},
journal= {arXiv preprint arXiv:1309.0706},
year = {2013}
}
Comments
Final report a the project "Classical Realizability, Categories and Games Theory" of ANII-Uruguay